summaryrefslogtreecommitdiff
path: root/test/regress/regress1/nl/sin1-sat.smt2
blob: d6275c6e8c95339eee5b4c9b6067c9e7e5feea06 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
; EXPECT: sat
(set-logic QF_NRA)
(set-info :status unsat)
(declare-fun x () Real)

(assert (> (sin 1) 0.84))
(assert (< (sin 1) 0.85))
(assert (< (- x (sin 1)) 0.000001))
(assert (< (- (sin 1) x) 0.000001))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback