blob: 8bcdfdfbccf70712727a53218ee39548b48ed7ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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)
|
