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 (member x (union A B)))

(assert (not (member x (intersection A B))))
(assert (not (member x (setminus A B))))
;(assert (not (member x (setminus B A))))
;(assert (member x B))

(check-sat)