summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-03-06 16:53:16 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2014-03-07 23:48:08 -0500
commit01cff049fac316d84ee05f747975a26b04e9c3a2 (patch)
tree6c6a5fdf1654a5bb4406ddde0a79ca78c3dc1a22 /test
parent7f604fe97bd85efbe6ffcf17140905cdb34c7468 (diff)
Fix run_regression on Mac.
Diffstat (limited to 'test')
-rwxr-xr-xtest/regress/run_regression10
1 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression
index ec9e17057..bf4dcc6ef 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -197,8 +197,8 @@ fi
check_models=false
if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then
- if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null &&
- ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then
+ if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then
# later on, we'll run another test with --check-models on
check_models=true
fi
@@ -207,9 +207,9 @@ check_proofs=false
if [ "$proof" = yes ]; then
# proofs not currently supported in incremental mode, turn it off
if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then
- if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs\>' &>/dev/null &&
- ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs\>' &>/dev/null &&
- ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental\>' &>/dev/null &&
+ if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null &&
+ ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then
# later on, we'll run another test with --check-proofs on
check_proofs=true
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback