diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-04 22:23:53 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-04 22:23:53 +0000 |
| commit | 5e2f381b26d683691d9a040589536dc39c5831e0 (patch) | |
| tree | 7fadaed04fa7f2954fe84efa78754a4fded30a33 /test | |
| parent | 1891eb9abf6e37a34c732211a8f11d08720fb2b7 (diff) | |
fix gdb issues (at least for static builds); resolves bug 194
Diffstat (limited to 'test')
| -rwxr-xr-x | test/regress/run_regression | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index b26792a78..ebef82cf1 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" --segv-nospin `basename "$benchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" |