diff options
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 084df6ac9..b740e8486 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -164,21 +164,35 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then fi command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` elif expr "$benchmark" : '.*\.p$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1; + proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP; lang=tptp + command_line=--finite-model-find expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then - error "cannot determine expected output of \`$benchmark': " \ - "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" + if grep -q '^% Status *: ' "$benchmark"; then + expected_output="$(grep '^% *Status *: ' "$benchmark" | head -1 | awk '{print$NF}')" + case "$expected_output" in + Theorem|Unsatisfiable) expected_exit_status=20 ;; + CounterSatisfiable|Satisfiable) expected_exit_status=10 ;; + GaveUp) expected_exit_status=0 ;; + esac + expected_output="% SZS status $expected_output for $(basename "$benchmark" | sed 's,\.p$,,')" + else + error "cannot determine expected output of \`$benchmark': " \ + "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" + fi + else + expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,') + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` fi - expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,') - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` 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: ,,'` + if grep -q '^% COMMAND-LINE: ' "$benchmark"; then + command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` + fi else error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p" fi |