blob: 0dee0e84de55f6a316818b05682d1e8d7529b41d (
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
|
% EXPECT: sat
OPTION "logic" "ALL_SUPPORTED";
IntPair: TYPE = [ INT, INT];
SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ];
x : SET OF IntPair;
y : SET OF IntPair;
w : SET OF IntPair;
z : SET OF SetIntPair;
a : IntPair;
b : IntPair;
ASSERT NOT a = b;
ASSERT a IS_IN x;
ASSERT b IS_IN y;
ASSERT b IS_IN w;
ASSERT (x,y) IS_IN z;
ASSERT (w,x) IS_IN z;
ASSERT NOT ( (x,x) IS_IN (z JOIN z) );
ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z);
CHECKSAT;
|
