From f2e126e7b2d48a9a12f854300f0711a8c0462d23 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 13 Apr 2018 15:53:44 -0700 Subject: [PATCH] Fix issue in regression script when proofs enabled (#1770) There were two issues in the new Python regression script when proofs were enabled: It would try to run "--check-proofs" on SAT benchmarks and the parameters added to check unsat cores were wrong. This commit fixes both issues. --- test/regress/run_regression.py | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index c861b0d71..1e3848338 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -210,7 +210,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path): if re.search(r'^(sat|invalid|unknown)$', expected_output) and \ '--no-check-models' not in basic_command_line_args: extra_command_line_args = ['--check-models'] - if proof and re.search(r'^(sat|valid)$', expected_output): + if proof and re.search(r'^(unsat|valid)$', expected_output): if '--no-check-proofs' not in basic_command_line_args and \ '--incremental' not in basic_command_line_args and \ '--unconstrained-simp' not in basic_command_line_args and \ @@ -223,10 +223,7 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path): '--incremental' not in basic_command_line_args and \ '--unconstrained-simp' not in basic_command_line_args and \ not cvc4_binary.endswith('pcvc4'): - extra_command_line_args = [ - '--check-proofs', '--no-bv-eq', '--no-bv-ineq', - '--no-bv-algebraic' - ] + extra_command_line_args += ['--check-unsat-cores'] if extra_command_line_args: command_line_args_configs.append( basic_command_line_args + extra_command_line_args) -- 2.30.2