blob: 39564c4cfae7cd122f8a8fb1714ad8e97317b137 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
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 (b > (d -1));
ASSERT (b < (d+1));
%ASSERT (2,3) IS_IN ((x JOIN x) JOIN x);
%ASSERT NOT (2, 3) IS_IN (TCLOSURE x);
ASSERT y = (TCLOSURE x);
ASSERT NOT ((1, 1) IS_IN y);
CHECKSAT;
|
