blob: c3dbb2cd612e633bdec6dd281f880377865a0ed4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
% EXPECT: sat
OPTION "fmf-bound";
OPTION "sets-ext";
Atom : TYPE;
REAL_UNIVERSE : SET OF [REAL];
ATOM_UNIVERSE : SET OF [Atom];
ASSERT REAL_UNIVERSE = UNIVERSE :: SET OF [REAL];
ASSERT ATOM_UNIVERSE = UNIVERSE :: SET OF [Atom];
levelVal : SET OF [Atom, REAL];
ASSERT FORALL (s : Atom, v1, v2 : REAL) :
(TUPLE(s) IS_IN ATOM_UNIVERSE AND TUPLE(v1) IS_IN REAL_UNIVERSE AND TUPLE(v2) IS_IN REAL_UNIVERSE)
=> (((s, v1) IS_IN levelVal AND (s, v2) IS_IN levelVal) => (v1 = v2));
CHECKSAT;
|