test/regress/regress0/rels/atom_univ2.cvc


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;