test/regress/regress1/rels/bv1p-sat.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

% EXPECT: sat
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;

ASSERT DISTINCT ( a, b );
ASSERT DISTINCT ( c, d );

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));


CHECKSAT;