test/regress/regress0/bug586.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
25
26

% EXPECT: sat
%%%
%%% DATA TYPES DEFINITIONS
%%%

%%% the roles
DATATYPE
	role = r1 | r2 | r3
	%%% adding two more roles ( | r4 | r5 ) to the type, but never referring to them make things work
END;

%%% structured datatypes
roleSet: TYPE = SET OF role;
roleGammaSet: TYPE = [# pos: roleSet, neg: roleSet #];
delta: TYPE = ARRAY role OF roleGammaSet;

emptyRoleSet : roleSet;
ASSERT emptyRoleSet = {} :: SET OF role;

d: delta;
ASSERT d[r3].pos = {r1};
ASSERT d[r2].pos = {r2,r3};
ASSERT d[r2].neg = {r1};

CHECKSAT;
%COUNTEREXAMPLE;