summaryrefslogtreecommitdiff
path: root/test/regress/run_regression
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/run_regression')
-rwxr-xr-xtest/regress/run_regression3
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 9204fe33c..868a69116 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -335,7 +335,8 @@ if $check_models || $check_proofs || $check_unsat_cores; then
check_cmdline="$check_cmdline --check-models"
fi
if $check_proofs; then
- check_cmdline="$check_cmdline --check-proofs"
+ # taking: Make the extra flags part of --check-proofs.
+ check_cmdline="$check_cmdline --check-proofs --no-bv-eq --no-bv-ineq --no-bv-algebraic"
fi
if $check_unsat_cores; then
check_cmdline="$check_cmdline --check-unsat-cores"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback