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";
OPTION "sets-ext";
Atom: TYPE;
x : SET OF [Atom, Atom];
y : SET OF [Atom, Atom];
r : SET OF [Atom, Atom];
t : SET OF [Atom];
a : Atom;
b : Atom;
c : Atom;
d : Atom;
e : Atom;
f : Atom;
g : Atom;
ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2);
ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3);
%ASSERT y = {(f, g), (b, c), (d, e), (c, e)};
ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)};
ASSERT (a, f) IS_IN x;
ASSERT (a, f) IS_IN y;
ASSERT x = y;
ASSERT NOT(a = b);
ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2));
ASSERT f = d;
CHECKSAT;
|
