diff options
Diffstat (limited to 'test/regress/regress0/bug605.cvc')
-rw-r--r-- | test/regress/regress0/bug605.cvc | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc index 1ccf7fa9e..564464931 100644 --- a/test/regress/regress0/bug605.cvc +++ b/test/regress/regress0/bug605.cvc @@ -1,30 +1,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;
+% 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; |