diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/bug217.smt2 (renamed from test/regress/regress0/uf/bug217.smt2) | 6 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output1.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung10_itesdk_output2.smt2 | 30 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output1.smt2 | 14 | ||||
-rw-r--r-- | test/regress/regress0/hung13sdk_output2.smt2 | 14 |
6 files changed, 98 insertions, 3 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) |