From: Andres Noetzli Date: Fri, 13 Apr 2018 22:53:44 +0000 (-0700) Subject: Fix issue in regression script when proofs enabled (#1770) X-Git-Tag: cvc5-1.0.0~5156 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f2e126e7b2d48a9a12f854300f0711a8c0462d23;p=cvc5.git 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. --- 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)