7 files changed, 100 insertions, 5 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 4789b0a55..6af6fbf70 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -49,7 +49,11 @@ SMT2_TESTS = \
 	simple-uf.smt2 \
 	simplification_bug4.smt2 \
 	parallel-let.smt2 \
-	get-value-incremental.smt2
+	get-value-incremental.smt2 \
+	hung13sdk_output1.smt2 \
+	hung10_itesdk_output2.smt2 \
+	hung10_itesdk_output1.smt2 \
+	hung13sdk_output2.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \
@@ -116,6 +120,7 @@ BUG_TESTS = \
 	bug168.smt \
 	bug187.smt2 \
 	bug216.smt2 \
+	bug217.smt2 \
 	bug220.smt2 \
 	bug239.smt \
 	bug274.cvc \
diff --git a/test/regress/regress0/uf/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 45f0f3c0c..92b72c87d 100644
--- a/test/regress/regress0/uf/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,10 +1,12 @@
+; EXPECT: unsat
+; EXIT: 20
 (set-logic QF_UF)
-(set-info :status unsat)
+(set-info :status sat)
+(set-option :produce-models true)
 (declare-fun f (Bool) Bool)
 (declare-fun x () Bool)
 (declare-fun y () Bool)
 (declare-fun z () Bool)
-;(assert (and x (or (f x) (f y))))
 (assert (or (f x) (f y) (f z)))
 (assert (not (f false)))
 (assert (not (f true)))
diff --git a/test/regress/regress0/hung10_itesdk_output1.smt2 b/test/regress/regress0/hung10_itesdk_output1.smt2
new file mode 100644
index 000000000..8bcdfdfbc
--- /dev/null
+++ b/test/regress/regress0/hung10_itesdk_output1.smt2
@@ -0,0 +1,30 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+  ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2
new file mode 100644
index 000000000..8bcdfdfbc
--- /dev/null
+++ b/test/regress/regress0/hung10_itesdk_output2.smt2
@@ -0,0 +1,30 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( declare-fun x4 () Bool)
+( declare-fun x5 () Real)
+( declare-fun x6 () Real)
+( declare-fun x7 () Real)
+( declare-fun x8 () Real)
+( declare-fun bo1 () Bool)
+( declare-fun bo2 () Bool)
+( declare-fun bo3 () Bool)
+( declare-fun r1 () Real)
+( declare-fun r2 () Real)
+( declare-fun r3 () Real)
+( define-fun myBoolIte ( ( a Real) ( b Bool) ( c Bool)) Bool
+  ( ite ( > a 0.0) b c))
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun f ( Real Bool) Real)
+( declare-fun fRealRealReal ( Real Real) Real)
+( declare-fun fRealReal ( Real) Real)
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung13sdk_output1.smt2 b/test/regress/regress0/hung13sdk_output1.smt2
new file mode 100644
index 000000000..bf3ab9a26
--- /dev/null
+++ b/test/regress/regress0/hung13sdk_output1.smt2
@@ -0,0 +1,14 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/hung13sdk_output2.smt2 b/test/regress/regress0/hung13sdk_output2.smt2
new file mode 100644
index 000000000..bf3ab9a26
--- /dev/null
+++ b/test/regress/regress0/hung13sdk_output2.smt2
@@ -0,0 +1,14 @@
+( set-logic QF_ALL_SUPPORTED)
+( set-info :source | SMT-COMP'06 organizers |)
+( set-info :smt-lib-version 2.0)
+( set-info :category "check")
+( set-info :status sat)
+( declare-fun x1 () Bool)
+( declare-fun x2 () Real)
+( declare-fun x3 () Real)
+( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
+  ( ite a1 b1 c1))
+( declare-fun fReal () Real)
+( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
+(check-sat)
+(exit)
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 9333cdb8c..68c1e0677 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -121,12 +121,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; 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
+  elif grep '^ *( *set-info  *:status  *sat' "$benchmark" &>/dev/null; then
     expected_proof=
     expected_output=sat
     expected_exit_status=10
     command_line=
-  elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
+  elif grep '^ *( *set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
     expected_proof=
     expected_output=unsat
     expected_exit_status=20