diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-04-05 20:07:30 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-04-05 20:07:30 +0000 |
| commit | f42542012fa0e59bdcca2b3f4c39b1a575d62140 (patch) | |
| tree | d6a15a5a40fa1e7cc7c9887811ba9b8c0220093b /test/regress/run_regression | |
| parent | 6076dfbf7f9f9be43f6c95cdfa4e292decc87baa (diff) | |
Support to test the "dumper" mechanism in regressions (feeding dump output back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 75d81b938..81570e817 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -5,7 +5,7 @@ # # usage: # -# run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ] +# run_regression cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ] # # Runs benchmark and checks for correct exit status and output. # @@ -13,14 +13,18 @@ prog=`basename "$0"` if [ $# -lt 2 -o $# -gt 3 ]; then - echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 + echo "usage: $prog cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2 exit 1 fi proof=no +dump=no if [ $1 = --proof ]; then proof=yes shift +elif [ $1 = --dump ]; then + dump=yes + shift fi cvc4=$1 @@ -179,11 +183,19 @@ if [ -z "$cvc4dirfull" ]; then fi cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" -echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] -( cd `dirname "$benchmark"`; - "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`; - echo $? >"$exitstatusfile" -) > "$outfile" 2> "$errfile" +if [ $dump = no ]; then + echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] + ( cd `dirname "$benchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" + ) > "$outfile" 2> "$errfile" +else + echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` \| $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 - [from working dir `dirname "$benchmark"`] + ( cd `dirname "$benchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --preprocess-only --dump=clauses --output-lang=smt2 -q --segv-nospin `basename "$benchmark"` | $cvc4full $CVC4_REGRESSION_ARGS $command_line --lang=smt2 -; + echo $? >"$exitstatusfile" + ) > "$outfile" 2> "$errfile" +fi diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` diffexit=$? |