summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sqrt2-sort-inf-unk.smt2
blob: f4b15020acf57caa324fc8750ee58fc1ecd00404 (plain) 
1
2
3
4
5
6

; COMMAND-LINE: --sort-inference
; EXPECT: unknown
(set-logic QF_NRA)
(declare-fun x () Real)
(assert (= (* x x) 2.0))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback