test/regress/regress0/bug605.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
27
28
29
30

% EXPECT: sat
OPTION "produce-models";

% GeoLocation
GeoLocation: TYPE = [# longitude: INT, latitude: INT #];

% Stationary object
StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
Facet: TYPE = [# base: StationaryObject #];

Segment: TYPE = [# s_f: Facet #];
A : TYPE = ARRAY INT OF Segment;
a : A;

p1: GeoLocation = (# longitude := 0, latitude := 0 #);

s1: StationaryObject = (# geoLoc := {p1} #);


f0: Facet = (# base := s1 #);


init: (A, INT, Facet) -> BOOLEAN
  = LAMBDA (v: A, i: INT, f: Facet): 
    v[0].s_f = f;
    
    
ASSERT (init(a, 2, f0));

CHECKSAT TRUE;