Support for failing .smt and .smt2 regressions (and other examples with

additional output).  If the benchmark file has '% EXPECT: ' gestures,
like for cvc regressions, that is used (after being stripped out so that
the cvc4 smt parser never sees these special lines).  However, this can
be a pain, since then you can't run the regression manually on the
command line (since it fails to parse).  So if there is another file
in the same directory as $benchmark called $benchmark.expect, that is
scanned for '% EXPECT: ' etc., and the benchmark file is used verbatim.

diff --git a/test/regress/run_regression b/test/regress/run_regression
index b4fc43be643143fee60123dfb8a05876680d17ee..b26792a7830141e66cc64bfada3face0fc3c1268 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -34,7 +34,14 @@ fi
 
 tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
-  if grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then
+  if test -e "$benchmark.expect"; 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: ,,'`
+    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
     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: ,,'`
@@ -54,7 +61,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
-  if grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" "$benchmark"; then
+  if test -e "$benchmark.expect"; 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: ,,'`
+    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
     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: ,,'`