test/regress/regress1/nl/approx-sqrt.smt2

   1 ; COMMAND-LINE: --no-check-models
   2 ; EXPECT: sat
   3 (set-logic QF_NRA)
   4 (set-info :status sat)
   5 (declare-fun x () Real)
   6 (assert (= (* x x) 2))
   7 (assert (> x 0))
   8 (assert (> (+ (* x x) (* (- 2.8) x)) (- 1.9598)))
   9 (assert (> (+ (* x x) (* (- 2.8284271247) x)) (- 1.9999999999999)))
  10 (assert (> (+ (* x x) (* (- 2.82842712475) x)) (- 2.00000001)))
  11 (check-sat)