blob: ed9fdce1f3512b28f0433c95f3ae17df572cad22 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
% COMMAND-LINE: --jh-rlv-order
% EXPECT: unsat
% note we require jh-rlv-order on this benchmark to avoid a proof failure currently (7/7/21)
OPTION "logic" "ALL";
BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
x : SET OF BvPair;
y : SET OF BvPair;
a : BvPair;
b : BvPair;
c : BvPair;
d : BvPair;
e : BvPair;
ASSERT DISTINCT ( a, b );
ASSERT DISTINCT ( c, d, e );
ASSERT a IS_IN x;
ASSERT b IS_IN x;
ASSERT a IS_IN y;
ASSERT b IS_IN y;
ASSERT (NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)) AND NOT ( e IS_IN (x JOIN y)) );
CHECKSAT;
|
