diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-13 15:53:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-13 15:53:44 -0700 |
commit | f2e126e7b2d48a9a12f854300f0711a8c0462d23 (patch) | |
tree | 932d0ec354c74c75cf96ddeaa15c3b434d50c2a9 /test/regress/run_regression.py | |
parent | 781bfd65daec2932b7836259b3484ac500edb46a (diff) |
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.
Diffstat (limited to 'test/regress/run_regression.py')
-rwxr-xr-x | test/regress/run_regression.py | 7 |
1 files 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) |