projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
9e15c81
)
don't do extra-checking for all regressions; that's probably a bad default
author
Morgan Deters
<mdeters@gmail.com>
Sun, 4 Jul 2010 04:04:23 +0000
(
04:04
+0000)
committer
Morgan Deters
<mdeters@gmail.com>
Sun, 4 Jul 2010 04:04:23 +0000
(
04:04
+0000)
test/regress/run_regression
patch
|
blob
|
history
diff --git
a/test/regress/run_regression
b/test/regress/run_regression
index a6ea0797b1cc5a943f8fde350faca0f92fc323e6..b26792a7830141e66cc64bfada3face0fc3c1268 100755
(executable)
--- 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"