summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug605.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bug605.cvc')
-rw-r--r--test/regress/regress0/bug605.cvc60
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback