diff options
author | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
commit | 859ae93590062ba7fef5577c6577068f0b74c239 (patch) | |
tree | 81d2d257c28414d10a261c242c1801f3eaadce78 /test/regress/regress0/bug605.cvc | |
parent | b455f5cde8b84b7951d309604b75a76afd8b8bfa (diff) |
Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
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; |