summaryrefslogtreecommitdiff
path: root/test/regress/run_regression
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2016-01-26 16:04:26 -0800
committerLiana Hadarean <lianahady@gmail.com>2016-01-26 16:04:26 -0800
commit42b665f2a00643c81b42932fab1441987628c5a5 (patch)
treeaa851e1fc4828f5a4d94ce0c11fa6d2d1199636f /test/regress/run_regression
parent7006d5ba2f68c01638a2ab2c98a86b41dcf4467c (diff)
Merged bit-vector and uf proof branch.
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