allow OOM for old AutoQ

fmlab-iis · Oct 18, 2024 · aa5e447 · aa5e447
1 parent e8314d5
commit aa5e447
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 6 deletions.
diff --git a/POPL25/Evaluation/non-parameterized/gen_table_correct.py b/POPL25/Evaluation/non-parameterized/gen_table_correct.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         assert data['result'] != 'V'
                         assert data['total'].count('/') == data['result'].count('/')
                         if '/' in data['total']:

diff --git a/POPL25/Evaluation/non-parameterized/gen_table_flipgate.py b/POPL25/Evaluation/non-parameterized/gen_table_flipgate.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         assert data['result'] == 'V' or data['result'] == 'V/V'
                         if '/' in data['result']:
                             data['result'] = format_duration(parse_duration(str(data['total'].split('/')[0]))) + '/' + format_duration(parse_duration(str(data['total'].split('/')[1])))

diff --git a/POPL25/Evaluation/non-parameterized/gen_table_missgate.py b/POPL25/Evaluation/non-parameterized/gen_table_missgate.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         if ('OEGrover' in file and data['result'] != '0') or ('OEGrover' not in file and 'V' not in data['result']):
                             data['result'] = 'WRONG'
                         else:

diff --git a/POPL25/Kick-the-Tires/non-parameterized/gen_table_correct.py b/POPL25/Kick-the-Tires/non-parameterized/gen_table_correct.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         assert data['result'] != 'V'
                         assert data['total'].count('/') == data['result'].count('/')
                         if '/' in data['total']:

diff --git a/POPL25/Kick-the-Tires/non-parameterized/gen_table_flipgate.py b/POPL25/Kick-the-Tires/non-parameterized/gen_table_flipgate.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         assert data['result'] == 'V' or data['result'] == 'V/V'
                         if '/' in data['result']:
                             data['result'] = format_duration(parse_duration(str(data['total'].split('/')[0]))) + '/' + format_duration(parse_duration(str(data['total'].split('/')[1])))

diff --git a/POPL25/Kick-the-Tires/non-parameterized/gen_table_missgate.py b/POPL25/Kick-the-Tires/non-parameterized/gen_table_missgate.py
@@ -137,7 +137,7 @@ def json_to_latex_table(tool_list, latex_filename):
                 if data['result'] == '1' or data['result'] == 'O':
                     data['result'] = data['total']
                 elif 'autoq' in tool:
-                    if data['result'] != 'TIMEOUT':
+                    if data['result'] not in ('TIMEOUT', 'ERROR'):
                         if ('OEGrover' in file and data['result'] != '0') or ('OEGrover' not in file and 'V' not in data['result']):
                             data['result'] = 'WRONG'
                         else: