blob: e01d99dee3fea0480388fb69cb7c65c1987b3c83 (
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: unsat
OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
Atom: TYPE;
a : SET OF [Atom];
b : SET OF [Atom, Atom];
x : Atom;
y : Atom;
ASSERT NOT(x = y);
ASSERT TUPLE(y) IS_IN a;
ASSERT (x, y) IS_IN b;
ASSERT UNIVERSE::SET OF [Atom, Atom] = (UNIVERSE::SET OF [Atom] PRODUCT UNIVERSE::SET OF [Atom]);
u : SET OF [Atom, Atom];
ASSERT u = UNIVERSE::SET OF [Atom, Atom];
ASSERT NOT (x, y) IS_IN u;
CHECKSAT;
|