diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 18 | ||||
-rw-r--r-- | test/regress/regress0/bug216.smt2.expect | 4 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/test.00.cvc | 5 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/test.01.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/queries0.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/test12.cvc | 1 | ||||
-rwxr-xr-x | test/regress/run_regression | 22 |
7 files changed, 36 insertions, 17 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9f4fdce89..73901c328 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -22,8 +22,8 @@ SMT_TESTS = \ let2.smt \ simple.smt \ simple2.smt \ - simple-lra.smt \ - simple-rdl.smt \ + simple-lra.smt \ + simple-rdl.smt \ simple-uf.smt # Regression tests for SMT2 inputs @@ -31,16 +31,16 @@ SMT2_TESTS = \ ite2.smt2 \ ite3.smt2 \ ite4.smt2 \ - simple-lra.smt2 \ - simple-rdl.smt2 \ - simple-rdl-definefun.smt2 \ + simple-lra.smt2 \ + simple-rdl.smt2 \ + simple-rdl-definefun.smt2 \ simple-uf.smt2 # Regression tests for PL inputs CVC_TESTS = \ boolean-prec.cvc \ hole6.cvc \ - ite.cvc \ + ite.cvc \ logops.01.cvc \ logops.02.cvc \ logops.03.cvc \ @@ -48,8 +48,8 @@ CVC_TESTS = \ logops.05.cvc \ simple.cvc \ smallcnf.cvc \ - test11.cvc \ test9.cvc \ + test11.cvc \ uf20-03.cvc \ wiki.01.cvc \ wiki.02.cvc \ @@ -83,11 +83,13 @@ BUG_TESTS = \ bug167.smt \ bug168.smt \ bug187.smt2 \ + bug216.smt2 \ bug220.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug216.smt2.expect b/test/regress/regress0/bug216.smt2.expect new file mode 100644 index 000000000..9a8435b2d --- /dev/null +++ b/test/regress/regress0/bug216.smt2.expect @@ -0,0 +1,4 @@ +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: unsat +% EXIT: 20 diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc index 38d720227..f56abb386 100644 --- a/test/regress/regress0/push-pop/test.00.cvc +++ b/test/regress/regress0/push-pop/test.00.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --incremental x: BOOLEAN; PUSH; @@ -6,6 +7,6 @@ ASSERT x; CHECKSAT; POP; ASSERT (NOT x); -% EXPECT: unsat +% EXPECT: sat CHECKSAT; -% EXIT: 20 +% EXIT: 10 diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc index 90be7d784..5d492db32 100644 --- a/test/regress/regress0/push-pop/test.01.cvc +++ b/test/regress/regress0/push-pop/test.01.cvc @@ -1,3 +1,5 @@ +% COMMAND-LINE: --incremental + x, y: BOOLEAN; ASSERT (x OR y); diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc index 110984083..c951aaf2e 100644 --- a/test/regress/regress0/queries0.cvc +++ b/test/regress/regress0/queries0.cvc @@ -1,4 +1,5 @@ % Tests the invariants for multiple queries. +% COMMAND-LINE: --incremental a, b: BOOLEAN; diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc index 25245f36a..55212bb07 100644 --- a/test/regress/regress0/test12.cvc +++ b/test/regress/regress0/test12.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --incremental % EXPECT: invalid % EXPECT: invalid % EXPECT: invalid diff --git a/test/regress/run_regression b/test/regress/run_regression index 614f02f0f..9c0eaa9db 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -38,15 +38,17 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'` + command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then + elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` + command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt - grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark" + 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" fi @@ -54,9 +56,11 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then expected_output=sat expected_exit_status=10 + command_line= elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then expected_output=unsat expected_exit_status=20 + command_line= else error "cannot determine status of \`$benchmark'" fi @@ -65,16 +69,17 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,'` + command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi - benchmark=$tmpbenchmark - elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then + elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` + command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt2 - grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark" + 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" fi @@ -82,9 +87,11 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then elif grep '^ *(set-info *:status *sat' "$benchmark" &>/dev/null; then expected_output=sat expected_exit_status=10 + command_line= elif grep '^ *(set-info *:status *unsat' "$benchmark" &>/dev/null; then expected_output=unsat expected_exit_status=20 + command_line= else error "cannot determine status of \`$benchmark'" fi @@ -99,6 +106,7 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi + command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2" fi @@ -130,9 +138,9 @@ if [ -z "$cvc4dirfull" ]; then fi cvc4base=`basename "$cvc4"` cvc4full="$cvc4dirfull/$cvc4base" -echo running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"` +echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`] ( cd `dirname "$benchmark"`; - "$cvc4full" $CVC4_REGRESSION_ARGS --segv-nospin `basename "$benchmark"`; + "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --segv-nospin `basename "$benchmark"`; echo $? >"$exitstatusfile" ) > "$outfile" 2> "$errfile" |