( 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)