From 1bba8bcace3505cc9a3ba7d0cda6339c00217595 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 14 Apr 2018 02:27:44 -0700 Subject: [PATCH] [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. --- test/regress/run_regression.py | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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 -- 2.30.2