added the ability to add custom expected stdout, stderr, and exit codes to smt and...

diff --git a/test/regress/regress0/ite2.smt2 b/test/regress/regress0/ite2.smt2
index ada94531d3d1e1d5e2861d8d6c4a1eeef8378d1a..9bcac2ec84956d5472a24ba400ff3807f2bd5fa1 100644 (file)
--- a/test/regress/regress0/ite2.smt2
+++ b/test/regress/regress0/ite2.smt2
@@ -1,3 +1,7 @@
+% EXPECT-ERROR: Outstanding case split in theory arith
+% EXPECT-ERROR: Outstanding case split in theory arith
+% EXPECT: SAT
+% EXIT: 10
 (set-logic QF_LRA)
 (set-info :status sat)
 (declare-fun x () Real)

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 9003479e75d8a56785be128304bda5cfe849abe1..b4fc43be643143fee60123dfb8a05876680d17ee 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -32,8 +32,19 @@ if ! [ -r "$benchmark" ]; then
   error "\`$benchmark' doesn't exist or isn't readable" >&2
 fi
 
+tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
-  if grep '^ *:status  *sat' "$benchmark" &>/dev/null; then
+  if 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: ,,'`
+    tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt
+    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark"
+    if [ -z "$expected_exit_status" ]; then
+      error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+    fi
+    benchmark=$tmpbenchmark
+  elif grep '^ *:status  *sat' "$benchmark" &>/dev/null; then
     expected_output=SAT
     expected_exit_status=10
   elif grep '^ *:status  *unsat' "$benchmark" &>/dev/null; then
@@ -43,7 +54,17 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
-  if grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
+  if 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: ,,'`
+    tmpbenchmark=`mktemp -t cvc4_benchmark.XXXXXXXXXX`.smt2
+    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\): ' "$benchmark" >"$tmpbenchmark"
+    if [ -z "$expected_exit_status" ]; then
+      error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
+    fi
+    benchmark=$tmpbenchmark
+  elif grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
     expected_output=SAT
     expected_exit_status=10
   elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
@@ -94,6 +115,7 @@ if [ -z "$cvc4dirfull" ]; then
 fi
 cvc4base=`basename "$cvc4"`
 cvc4full="$cvc4dirfull/$cvc4base"
+echo  running $cvc4full `basename "$benchmark"` from `dirname "$benchmark"`
 ( cd `dirname "$benchmark"`;
   "$cvc4full" --segv-nospin `basename "$benchmark"`;
   echo $? >"$exitstatusfile"
@@ -110,6 +132,7 @@ rm -f "$experrfile"
 rm -f "$outfile"
 rm -f "$errfile"
 rm -f "$exitstatusfile"
+test -n "$tmpbenchmark" && rm -f "$tmpbenchmark"
 
 exitcode=0
 if [ $diffexit -ne 0 ]; then