blob: 95fb5f02cf3a053546f61ef31132362b9101cbda (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
% EXPECT: unsat
OPTION "logic" "ALL";
DATATYPE unit = u END;
BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;
a : BITVECTOR(1);
b : BITVECTOR(1);
c : BITVECTOR(1);
d : BITVECTOR(1);
e : BITVECTOR(1);
ASSERT NOT ( b = c );
ASSERT (a, u, b) IS_IN x;
ASSERT (a, u, c) IS_IN x;
ASSERT (d, u, a) IS_IN y;
ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y));
CHECKSAT;
|
