summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/proj-issue343.smt2
blob: 6d2971ad8aff6122f6b6941143b1fe1d994ef8d5 (plain) 
1
2
3
4
5
6
7

; EXPECT: sat
; COMMAND-LINE: --no-check-models
(set-logic ALL)
(set-option :solve-bv-as-int bv)
(declare-const _x8 Real)
(assert (distinct real.pi _x8))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback