test/regress/regress0/bug605.cvc

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