summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/nta/exp-neg2-unsat-unsound.smt2
blob: 69c36179a1f20df1d1044f07d39c1780e7110796 (plain) 
1
2
3
4
5
6
7
8
9
10

; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
; EXPECT: sat
(set-logic QF_NRAT)
(declare-fun x () Real)
(assert (or 
(and (<= (exp x) 0.01) (= x (- 2.0)))
(and (> (exp x) 0.2) (= x (- 1.0)))
)
)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback