diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
commit | e66924cb0f425ca70969058532340e68c9c17a54 (patch) | |
tree | 6dfdb2d02621c45a17b9ca3202cc3db7c30d7da5 /test/regress/run_regression | |
parent | d5d504da7c73538642b9be86c73f8407e08ab57a (diff) |
SmtEngine now fails with a ModalException if --incremental is not enabled
but a push/pop or multiple query is attempted (previously it could give
incorrect answers)
Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).
Also fix mkbuilddir script for when it's called from contrib/switch-config.
Diffstat (limited to 'test/regress/run_regression')
-rwxr-xr-x | test/regress/run_regression | 22 |
1 files changed, 15 insertions, 7 deletions
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" |