diff --git a/scripts/get_exper_brunch_stat.py b/scripts/get_exper_brunch_stat.py index e0449c5b..e5896b52 100644 --- a/scripts/get_exper_brunch_stat.py +++ b/scripts/get_exper_brunch_stat.py @@ -15,7 +15,8 @@ "crab_time": "crab.time", "opsem_assert_time": "opsem.assert", "opsem_simplify_time": "opsem.simplify", - "seahorn_total_time": "seahorn_total" + "seahorn_total_time": "seahorn_total", + "object_domain_use_odi": "count.move_object" # ADD additional coloumn and corresponded pattern on outputs here } @@ -58,7 +59,7 @@ def read_brunchstat_from_log(log_file_name, use_crab=False): # stat_name = " ".join(stat[1:-1]) stat_num = stat[-1] for key in BRUNCH_DICT: - if stat[1] == BRUNCH_DICT[key]: + if stat[-2] == BRUNCH_DICT[key] or BRUNCH_DICT[key] in stat[-2]: row_dict[key] = stat_num line = log_file.readline() if cur_test: