diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-21 09:41:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-21 09:41:50 -0700 |
| commit | be2702490d684c100ba6abe76ee156078a9aa621 (patch) | |
| tree | 8b22bc7e38aad39da092b409dded4d2ce84b4047 /test/regress/run_regression | |
| parent | 8f0aae827e16f4dfcebb8dad2cc528649d40b16a (diff) | |
Fix various regression tests (#1657)
While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.). This was an issue with the tests that now
have a COMMAND-LINE directive.
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 6b2447d8e..4ae013911 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -146,9 +146,6 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` - if [ -z "$expected_exit_status" ]; then - expected_exit_status=0 - fi elif grep '^; \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\|SCRUBBER\|ERROR-SCRUBBER\): ' "$benchmark" "$benchmark" &>/dev/null; then scrubber=`grep '^; SCRUBBER: ' "$benchmark" | sed 's,^; SCRUBBER: ,,'` errscrubber=`grep '^; ERROR-SCRUBBER: ' "$benchmark" | sed 's,^; ERROR-SCRUBBER: ,,'` @@ -156,19 +153,28 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_error=`grep '^; EXPECT-ERROR: ' "$benchmark" | sed 's,^; EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^; EXIT: ' "$benchmark" | perl -pe 's,^; EXIT: ,,;s,\r,,'` command_line=`grep '^; COMMAND-LINE: ' "$benchmark" | sed 's,^; COMMAND-LINE: ,,'` - if [ -z "$expected_exit_status" ]; then - expected_exit_status=0 + fi + + # If expected output/error was not given, try to determine the status from + # the commands. + if [ -z "$expected_output" -a -z "$expected_error" ]; then + if grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then + expected_output=sat + elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then + expected_output=unsat fi - elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_output=sat - expected_exit_status=0 - command_line= - elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_output=unsat + fi + + # A valid test case needs at least an expected output (explicit or through + # SMT2 commands) or an expected exit status. + if [ -z "$expected_output" -a -z "$expected_error" -a -z "$expected_exit_status" ]; then + error "cannot determine status of \`$benchmark'" + fi + + # If no explicit expected exit status was given, we assume that the solver is + # supposed to succeed. + if [ -z "$expected_exit_status" ]; then expected_exit_status=0 - command_line= - else - error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then lang=cvc4 |