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.cvc30
1 files changed, 0 insertions, 30 deletions
diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc
deleted file mode 100644
index 564464931..000000000
--- a/test/regress/regress0/bug605.cvc
+++ /dev/null
@@ -1,30 +0,0 @@
-% 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