test/regress/regress0/bug605.cvc

   1 OPTION "produce-models";
   2
   3 % GeoLocation
   4 GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
   5
   6 % Stationary object
   7 StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
   8 Facet: TYPE = [# base: StationaryObject #];
   9
  10 Segment: TYPE = [# s_f: Facet #];
  11 A : TYPE = ARRAY INT OF Segment;
  12 a : A;
  13
  14 p1: GeoLocation = (# longitude := 0, latitude := 0 #);
  15
  16 s1: StationaryObject = (# geoLoc := {p1} #);
  17
  18
  19 f0: Facet = (# base := s1 #);
  20
  21
  22 init: (A, INT, Facet) -> BOOLEAN
  23   = LAMBDA (v: A, i: INT, f: Facet):
  24     v[0].s_f = f;
  25
  26
  27 ASSERT (init(a, 2, f0));
  28
  29 CHECKSAT TRUE;
  30 COUNTERMODEL;