Fix run_regression on Mac.
authorMorgan Deters <mdeters@cs.nyu.edu>
Thu, 6 Mar 2014 21:53:16 +0000 (16:53 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sat, 8 Mar 2014 04:48:08 +0000 (23:48 -0500)
test/regress/run_regression

index ec9e170578afa2c7c722fd9b3e1ecff5c05a3c15..bf4dcc6ef69ccc492d2f44c3ef5320a3f813cc1b 100755 (executable)
@@ -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