diff options
Diffstat (limited to 'test/regress/regress0/hung10_itesdk_output2.smt2')
| -rw-r--r-- | test/regress/regress0/hung10_itesdk_output2.smt2 | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/test/regress/regress0/hung10_itesdk_output2.smt2 b/test/regress/regress0/hung10_itesdk_output2.smt2 deleted file mode 100644 index 8bcdfdfbc..000000000 --- a/test/regress/regress0/hung10_itesdk_output2.smt2 +++ /dev/null @@ -1,30 +0,0 @@ -( 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) |