summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sets/issue5309.smt2
blob: 383b1263e049c25a9f00573264631ce0ce65d1bd (plain) 
1
2
3
4
5
6
7

(set-logic ALL)
(set-info :status sat)
(declare-const zero Int)
(declare-fun A () (Set Int))
(assert (exists ((x Int)) (= A (singleton x))))
(assert (member (- zero) A))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback