summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
blob: a7c2bec8df33ae9008c8e59ffdd3cd4c0ad2ad88 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

(set-logic ALL)
(set-info :status unsat)

(declare-fun x () Int)
(declare-fun y () Int)

(declare-fun S () (Set Int))
(declare-fun T () (Set Int))

(assert (member x S))

(assert (= S (union T (singleton y))))

(assert (not (= x y)))

(assert (not (member x T)))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback