; EXPECT: unsat
(set-logic QF_UFLIAFS)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun x () (Set Int))
(declare-fun y () (Set Int))
(assert (= x (singleton a)))
(assert (= y (singleton b)))
(assert (not (= x y)))
(assert (and (< 1 a) (< a 3) (< 1 b) (< b 3)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback