test/regress/regress0/bug339.smt2

   1 (set-logic QF_LRA)
   2 (set-info :status sat)
   3
   4 (declare-fun x () Real)
   5 (declare-fun P () Bool)
   6
   7 (assert
   8  (let ((y (ite P 1 x)))
   9    (and (not (= y 1))
  10         (> y 0)
  11         (<= y 1))))
  12
  13 (check-sat)
  14
  15 (exit)