summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
blob: 204af2f2d284103c3b5128623e7a6bd839189bb1 (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 (in x S))

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

(assert (not (= x y)))

(assert (not (in x T)))

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