diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/boolean.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/hole6.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/wiki.05.cvc | 2 | ||||
-rwxr-xr-x | test/regress/run_regression | 34 |
5 files changed, 28 insertions, 13 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 3a4583805..e564b567a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -45,6 +45,7 @@ SMT2_TESTS = \ # Regression tests for PL inputs CVC_TESTS = \ + boolean.cvc \ boolean-prec.cvc \ hole6.cvc \ ite.cvc \ diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index d6f428bdb..2d0eb59b2 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,5 +804,5 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 31204a6c1..ece29e17c 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,5 +177,5 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index 1aedcbe2b..04c7dafe0 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,5 +2,5 @@ a, b, c : BOOLEAN; % EXPECT: valid QUERY a OR (a AND b) <=> a; -% EXIT: 20 % PROOF +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index b836b39f6..6c06175d2 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -52,6 +52,8 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then + proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 + lang=smt if test -e "$benchmark.expect"; then expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` @@ -68,9 +70,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle - # this frustrates our auto-language-detection, so add explicit --lang + # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX - command_line="${command_line:+$command_line }--lang=smt" grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -90,6 +91,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then + proof_command='(get-proof)' + lang=smt2 if test -e "$benchmark.expect"; then expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` @@ -106,9 +109,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle - # this frustrates our auto-language-detection, so add explicit --lang + # this frustrates our auto-language-detection gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX - command_line="${command_line:+$command_line }--lang=smt2" grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark" if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -128,6 +130,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + proof_command='DUMP_PROOF;' + lang=cvc4 expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` @@ -145,6 +149,8 @@ else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2" fi +command_line="${command_line:+$command_line }--lang=$lang" + gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX gettemp outfile cvc4_stdout.$$.XXXXXXXXXX @@ -203,19 +209,27 @@ if [ "$exit_status" != "$expected_exit_status" ]; then fi if [ "$proof" = yes -a "$expected_proof" = yes ]; then - echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] - ( cd `dirname "$benchmark"`; - "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`; + gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX + cp "$benchmark" "$pfbenchmark"; + echo "$proof_command" >>"$pfbenchmark"; + echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] + ( cd `dirname "$pfbenchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" - if [ ! -s "$outfile" ]; then + gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX + diff --unchanged-group-format='' \ + --old-group-format='' \ + --new-group-format='%>' \ + "$expoutfile" "$outfile" > "$pfoutfile" + if [ ! -s "$pfoutfile" ]; then echo "$prog: error: proof generation failed with empty output (stderr follows)" cat "$errfile" exitcode=1 else - echo running $LFSC "$outfile" [from working dir `dirname "$benchmark"`] - if ! $LFSC "$outfile" &> "$errfile"; then + echo running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`] + if ! $LFSC "$pfoutfile" &> "$errfile"; then echo "$prog: error: proof checker failed (output follows)" cat "$errfile" exitcode=1 |