don't do extra-checking for all regressions; that's probably a bad default
authorMorgan Deters <mdeters@gmail.com>
Sun, 4 Jul 2010 04:04:23 +0000 (04:04 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sun, 4 Jul 2010 04:04:23 +0000 (04:04 +0000)
test/regress/run_regression

index a6ea0797b1cc5a943f8fde350faca0f92fc323e6..b26792a7830141e66cc64bfada3face0fc3c1268 100755 (executable)
@@ -132,7 +132,7 @@ cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
 echo  running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"`
 ( cd `dirname "$benchmark"`;
-  "$cvc4full" -d extra-checking --segv-nospin `basename "$benchmark"`;
+  "$cvc4full" --segv-nospin `basename "$benchmark"`;
   echo $? >"$exitstatusfile"
 ) > "$outfile" 2> "$errfile"