summaryrefslogtreecommitdiff
path: root/test/regress/regress0/issue5099-model-2.smt2
blob: 9feada28088bbc838513f3e22528b8b4dcde162c (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: -m -q
; EXPECT: sat
; EXPECT: ((IP true))
(set-logic QF_NRA)
(declare-const r11 Real)
(declare-const r16 Real)
(assert (! (distinct (/ 1 r16) r11) :named IP))
(check-sat)
(get-assignment)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback