summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sym/sym5.smt2
blob: 16b44d115545818a9798aab246116549c21c1a36 (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 A () (Set Int))
(declare-fun B () (Set Int))
(declare-fun C () (Set Int))

(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)

(assert (set.subset A (set.insert g h i (set.singleton f))))
(assert (= C (set.minus A B) ))
(assert (set.subset B A))
(assert (= C (set.inter A B)))
(assert (set.member j C))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback