[Reg] Make status/unsat-core detection more robust (#1775)

This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 3b97f6dde017d7b7693a877c64880935b54891a3..a45489d6a2aed4e01f1c9da2c1af8f4e9485f432 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -143,7 +143,13 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path):
     metadata_lines = None
     with open(metadata_filename, 'r') as metadata_file:
         metadata_lines = metadata_file.readlines()
-    metadata_content = ''.join(metadata_lines)
+
+    benchmark_content = None
+    if metadata_filename == benchmark_path:
+        benchmark_content = ''.join(metadata_lines)
+    else:
+        with open(benchmark_path, 'r') as benchmark_file:
+            benchmark_content = benchmark_file.read()
 
     # Extract the metadata for the benchmark.
     scrubber = None
@@ -178,7 +184,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path):
     if expected_output == '' and expected_error == '':
         match = None
         if status_regex:
-            match = re.search(status_regex, metadata_content)
+            match = re.search(status_regex, benchmark_content)
 
         if match:
             expected_output = status_to_output(match.group(1))
@@ -187,8 +193,8 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path):
             # been set explicitly, the benchmark is invalid.
             sys.exit('Cannot determine status of "{}"'.format(benchmark_path))
 
-    if not proof and ('(get-unsat-core)' in metadata_content
-                      or '(get-unsat-assumptions)' in metadata_content):
+    if not proof and ('(get-unsat-core)' in benchmark_content
+                      or '(get-unsat-assumptions)' in benchmark_content):
         print(
             '1..0 # Skipped: unsat cores not supported without proof support')
         return