blob: bf3ab9a26345cca64e328de06531d3ad312c0d43 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
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)
|
