summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sygus/issue3648.smt2
blob: 2fc1a6115f0ce23f9b84620ed24f375b49cf49c6 (plain) 
1
2
3
4
5
6
7

; EXPECT: sat
; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
(set-logic ALL)
(declare-fun a () Real)
(assert (> a 0.000001))
(assert (< (- (sin 1) a) 0.000001))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback