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

(set-logic ALL_SUPPORTED)
(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