blob: dc5c2f37dfe9724f094b4e91ce2ca7d2b38f1433 (
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";
IntPair: TYPE = [ INT, INT];
IntIntPair: TYPE = [ IntPair, IntPair];
x : SET OF IntIntPair;
y : SET OF IntIntPair;
z : SET OF IntPair;
w : SET OF IntPair;
a : IntPair;
b : IntPair;
c : IntIntPair;
ASSERT NOT a = b;
ASSERT a IS_IN z;
ASSERT b IS_IN z;
ASSERT (a,b) IS_IN x;
ASSERT (b,a) IS_IN x;
ASSERT c IS_IN x;
ASSERT NOT ( c = (a,b) ) AND NOT ( c = (b,a) );
CHECKSAT;
|
