blob: 824e7e1253fccc3afe5cd2ed9f57d8e6fe97188b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
; EXPECT: sat
(set-option :incremental false)
(set-logic ALL)
(declare-fun x () (Set (Tuple (_ BitVec 2) (_ BitVec 2))))
(declare-fun y () (Set (Tuple (_ BitVec 2) (_ BitVec 2))))
(declare-fun a () (_ BitVec 2))
(declare-fun b () (_ BitVec 2))
(declare-fun c () (_ BitVec 2))
(declare-fun d () (_ BitVec 2))
(declare-fun e () (_ BitVec 2))
(assert (not (= b c)))
(assert (member (mkTuple a b) x))
(assert (member (mkTuple a c) x))
(assert (member (mkTuple d a) y))
(assert (not (member (mkTuple a a) (join x y))))
(check-sat)
|
