From 522450336079fc0fef751876fa8c934369d608b3 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 4 Jul 2010 04:04:23 +0000 Subject: [PATCH] don't do extra-checking for all regressions; that's probably a bad default --- test/regress/run_regression | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/regress/run_regression b/test/regress/run_regression index a6ea0797b..b26792a78 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -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" -- 2.30.2