summaryrefslogtreecommitdiff
path: root/test/regress/regress0/nl/issue3652.smt2
blob: f3429b73decec0a216877ee8977a68ec90a4f5ac (plain) 
1
2
3
4
5
6
7

;COMMAND-LINE: --check-models
;EXIT: 1
;EXPECT: (error "Cannot run check-model on a model with approximate values.")
(set-logic QF_NRA)
(declare-fun a () Real)
(assert (= (* a a) 2))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback