fix bug 605

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 1f2963e183733820781202525e958e4fb017907c..5319e1e9806fc3cd7ce487f9c80dbbf3a04c1765 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -214,6 +214,8 @@ bool TypeNode::isComparableTo(TypeNode t) const {
       }
     }
     return true;
+  } else if(isSet() && t.isSet()) {
+    return getSetElementType().isComparableTo(t.getSetElementType());
   }
 
   if(isPredicateSubtype()) {

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 819e2176ea37274a478ddc319e4a897e44c1af35..f716b8b110f6db618b7d43e9581da1ba164856bc 100644 (file)
--- 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 (file)
index 0000000..5217c22
--- /dev/null
+++ b/test/regress/regress0/bug605.cvc
@@ -0,0 +1,30 @@
+OPTION "produce-models";\r
+\r
+% GeoLocation\r
+GeoLocation: TYPE = [# longitude: INT, latitude: INT #];\r
+\r
+% Stationary object\r
+StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];\r
+Facet: TYPE = [# base: StationaryObject #];\r
+\r
+Segment: TYPE = [# s_f: Facet #];\r
+A : TYPE = ARRAY INT OF Segment;\r
+a : A;\r
+\r
+p1: GeoLocation = (# longitude := 0, latitude := 0 #);\r
+\r
+s1: StationaryObject = (# geoLoc := {p1} #);\r
+\r
+\r
+f0: Facet = (# base := s1 #);\r
+\r
+\r
+init: (A, INT, Facet) -> BOOLEAN\r
+  = LAMBDA (v: A, i: INT, f: Facet): \r
+    v[0].s_f = f;\r
+    \r
+    \r
+ASSERT (init(a, 2, f0));\r
+\r
+CHECKSAT TRUE;\r
+COUNTERMODEL;
\ No newline at end of file