test/regress/regress1/rels/rel_tc_4.cvc


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

% EXPECT: unsat
OPTION "logic" "ALL";
IntPair: TYPE = [INT, INT];
x : SET OF IntPair;
y : SET OF IntPair;
a: INT;
b:INT;
c:INT;
d:INT;
ASSERT (1, a) IS_IN x;
ASSERT (1, c) IS_IN x;
ASSERT (1, d) IS_IN x;
ASSERT (b, 1) IS_IN x;
ASSERT (b = d);
ASSERT (2,b) IS_IN ((x JOIN x) JOIN x);
ASSERT NOT (2, 1) IS_IN TCLOSURE(x);


CHECKSAT;