diff options
Diffstat (limited to 'test/regress/regress0/hung13sdk_output2.smt2')
| -rw-r--r-- | test/regress/regress0/hung13sdk_output2.smt2 | 14 |
1 files changed, 14 insertions, 0 deletions
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) |