test/regress/regress0/hung13sdk_output1.smt2

   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
  10   ( ite a1 b1 c1))
  11 ( declare-fun fReal () Real)
  12 ( assert ( = 4.0 ( + fReal ( myRealIte x1 x2 x3))))
  13 (check-sat)
  14 (exit)