diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/non-fatal-errors.smt2 | 29 | ||||
| -rwxr-xr-x | test/regress/run_regression | 10 |
3 files changed, 41 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1368dd067..dbff6cff1 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -69,7 +69,8 @@ SMT2_TESTS = \ hung10_itesdk_output1.smt2 \ hung13sdk_output2.smt2 \ declare-funs.smt2 \ - declare-fun-is-match.smt2 + declare-fun-is-match.smt2 \ + non-fatal-errors.smt2 # Regression tests for PL inputs CVC_TESTS = \ diff --git a/test/regress/regress0/non-fatal-errors.smt2 b/test/regress/regress0/non-fatal-errors.smt2 new file mode 100644 index 000000000..1e1865883 --- /dev/null +++ b/test/regress/regress0/non-fatal-errors.smt2 @@ -0,0 +1,29 @@ +; SCRUBBER: sed 's/".*"/""/g' +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: success +; EXPECT: sat +(set-option :print-success true) +(set-option :produce-unsat-cores true) +(set-option :produce-models true) +(set-option :produce-proofs true) +(set-option :produce-assignments true) +(set-logic UF) +(declare-fun p () Bool) +(get-unsat-core) +(get-value (p)) +(get-proof) +(get-model) +(get-assignment) +(assert true) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index 536a3e8a5..5d4165597 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -130,6 +130,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then lang=smt2 + + # If this test case requires unsat cores but CVC4 is not built with proof + # support, skip it. Note: checking $CVC4_REGRESSION_ARGS instead of $proof + # here because $proof is not set for the second run. + requires_proof=`grep '(get-unsat-core)' "$benchmark"` + if [[ ! "$CVC4_REGRESSION_ARGS" = *"--proof"* ]] && [ -n "$requires_proof" ]; then + exit 77 + fi + if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` @@ -288,6 +297,7 @@ if [ "$proof" = yes ]; then fi fi fi + if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" |