1 ( set-logic QF_ALL_SUPPORTED)
2 ( set-info :source | SMT-COMP'06 organizers |)
3 ( set-info :smt-lib-version 2.0)
4 ( set-info :category "check")
5 ( set-info :status sat)
6 ( declare-fun x1 () Bool)
7 ( declare-fun x2 () Real)
8 ( declare-fun x3 () Real)
9 ( define-fun myRealIte ( ( a1 Bool) ( b1 Real) ( c1 Real)) Real
11 ( declare-fun fReal () Real)
12 ( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))