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


1
2
3
4
5
6
7
8
9
10
11
12
13

; COMMAND-LINE: --nl-ext-tplanes --no-check-proofs
; EXPECT: unsat
(set-logic QF_NRA)
(set-info :status unsat)
(declare-fun x () Real)
(assert (= (* x x) 2))
(assert (> x 0))
(assert (or 
(> (+ (* x x) (* (- 2.8) x)) (- 1.95))
(> (+ (* x x) (* (- 2.8284271247) x)) (- 1.999999))
(> (+ (* x x) (* (- 2.82842712475) x)) (- 2.0000000000000000000000000001))
))
(check-sat)