From bf69e71803eeab9ed3655b24cee597693f1b3ec0 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 27 May 2010 20:46:50 +0000
Subject: added the ability to add custom expected stdout, stderr, and exit
 codes to smt and smt2 regressions; resolves bug 132

---
 test/regress/regress0/ite2.smt2 |  4 ++++
 test/regress/run_regression     | 27 +++++++++++++++++++++++++--
 2 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/test/regress/regress0/ite2.smt2 b/test/regress/regress0/ite2.smt2
index ada94531d..9bcac2ec8 100644
--- 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 9003479e7..b4fc43be6 100755
--- 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
-- 
cgit v1.2.3