diff options
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 |