diff options
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index c141cf43a..2be776b3f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -56,8 +56,8 @@ expfile=`mktemp -t cvc4_expected.XXXXXXXXXX` outfile=`mktemp -t cvc4_output.XXXXXXXXXX` echo "$expected_output" >"$expfile" -echo "$cvc4" --segv-nospin "$benchmark" -"$cvc4" --segv-nospin "$benchmark" | tee "$outfile" +# echo "$cvc4" --segv-nospin "$benchmark" +"$cvc4" --segv-nospin "$benchmark" > "$outfile" diffs=`diff -u "$expfile" "$outfile"` diffexit=$? |