blob: 969d0d71c96442889d2e58bdb57d0d8e213eb1c1 (
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
27
28
29
30
31
32
33
34
|
% EXPECT: unsat
OPTION "logic" "ALL_SUPPORTED";
IntPair: TYPE = [INT, INT];
IntTup: TYPE = [INT];
x : SET OF IntPair;
y : SET OF IntPair;
r : SET OF IntPair;
w : SET OF IntTup;
z : SET OF IntTup;
r2 : SET OF IntPair;
a : IntPair;
ASSERT a = (3,1);
ASSERT a IS_IN x;
d : IntPair;
ASSERT d = (1,3);
ASSERT d IS_IN y;
e : IntPair;
ASSERT e = (4,3);
ASSERT r = (x JOIN y);
ASSERT TUPLE(1) IS_IN w;
ASSERT TUPLE(2) IS_IN z;
ASSERT r2 = (w PRODUCT z);
ASSERT NOT (e IS_IN r);
%ASSERT e IS_IN r2;
ASSERT (r <= r2);
ASSERT NOT ((3,3) IS_IN r2);
CHECKSAT;
|
