From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Sat, 14 Apr 2018 09:27:44 +0000 (-0700)
Subject: [Reg] Make status/unsat-core detection more robust (#1775)
X-Git-Tag: cvc5-1.0.0~5151
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1bba8bcace3505cc9a3ba7d0cda6339c00217595;p=cvc5.git

[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 3b97f6dde..a45489d6a 100755
--- 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