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