test/regress/regress0/sets/sets-new.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(define-sort SetInt () (Set Int))

(declare-fun A () SetInt)
(declare-fun B () SetInt)
(declare-fun x () Int)
(assert (set.member x (set.union A B)))

(assert (not (set.member x (set.intersection A B))))
(assert (not (set.member x (set.minus A B))))
;(assert (not (set.member x (set.minus B A))))
;(assert (set.member x B))

(check-sat)