test/regress/regress0/bug586.cvc

   1 % EXPECT: sat
   2 %%%
   3 %%% DATA TYPES DEFINITIONS
   4 %%%
   5
   6 %%% the roles
   7 DATATYPE
   8         role = r1 | r2 | r3
   9         %%% adding two more roles ( | r4 | r5 ) to the type, but never referring to them make things work
  10 END;
  11
  12 %%% structured datatypes
  13 roleSet: TYPE = SET OF role;
  14 roleGammaSet: TYPE = [# pos: roleSet, neg: roleSet #];
  15 delta: TYPE = ARRAY role OF roleGammaSet;
  16
  17 emptyRoleSet : roleSet;
  18 ASSERT emptyRoleSet = {} :: SET OF role;
  19
  20 d: delta;
  21 ASSERT d[r3].pos = {r1};
  22 ASSERT d[r2].pos = {r2,r3};
  23 ASSERT d[r2].neg = {r1};
  24
  25 CHECKSAT;
  26 %COUNTEREXAMPLE;