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

; COMMAND-LINE: -m
; 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