summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/issue3003.smt2
blob: 52bb2596394f4ec3d37efb41d25154a5067a530e (plain)
1
2
3
4
5
6
7
8
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_NRA)
(set-info :status sat)
(declare-fun _substvar_15_ () Real)                                                                                                                                 
(declare-fun _substvar_17_ () Real)                                                                                                                                 
(assert (let ((?v_1 (<= 0.0 _substvar_15_))) (and ?v_1 (and ?v_1 (and ?v_1 (= (* _substvar_15_ _substvar_15_) (+ 1 (* _substvar_17_ (* _substvar_17_ (- 1)))))))))) 
(check-sat)     
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback