diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-27 05:52:21 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-27 05:52:21 +0000 |
commit | 41fc06dc6352a847f047970e63e46455eb4dd050 (patch) | |
tree | 92f08943a4782f24f0cb44935d612b400a612592 /test/regress/regress0/hung13sdk_output2.smt2 | |
parent | b122cec27ca27d0b48e786191448e0053be78ed0 (diff) |
First chunk of boolean-terms support.
Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.
This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance.
(this commit was certified error- and warning-free by the test-and-commit script.)
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) |