From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 13 Dec 2013 15:41:37 +0000 (-0500)
Subject: Some minor cleanup.
X-Git-Tag: cvc5-1.0.0~6987^2~38
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ff3b510039f969966ba130abcfdb5f4077ec81c;p=cvc5.git

Some minor cleanup.
---

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 7c11c0d0a..b5116071a 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -236,17 +236,17 @@ fi
 cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
 if [ $dump = no ]; then
-  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
   time ( :; \
   ( cd `dirname "$benchmark"`;
-    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line `basename "$benchmark"`;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile" )
 else
-  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` \| $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q `basename "$benchmark"` \| $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`]
   time ( :; \
   ( cd `dirname "$benchmark"`;
-    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` | $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q `basename "$benchmark"` | $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile" )
 fi
@@ -285,10 +285,10 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then
       cp $benchmark $pfbenchmark
       echo "$proof_command" >>"$pfbenchmark";
   fi
-  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
+  echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
   time ( :; \
   ( cd `dirname "$pfbenchmark"`;
-    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`;
+    $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"`;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile" )