diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-08-18 22:06:28 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-08-19 13:27:41 -0400 |
| commit | ca72dd6bc0fdc63391b568e4cbcf289300e295dc (patch) | |
| tree | afb1742ae852eca166d19f172676173fbaa3ad6a /test | |
| parent | 331ec1abc311a6be85eb5adc0ca70f4e3c0c79a2 (diff) | |
fix bug 605
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bug605.cvc | 30 |
2 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 819e2176e..f716b8b11 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -175,6 +175,7 @@ BUG_TESTS = \ bug596.cvc \ bug596b.cvc #bug590.smt2 +#bug605.cvc %% fixes 605, but disabling as it runs into a different assertion failure TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc new file mode 100644 index 000000000..5217c2242 --- /dev/null +++ b/test/regress/regress0/bug605.cvc @@ -0,0 +1,30 @@ +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;
+COUNTERMODEL;
\ No newline at end of file |