From ca72dd6bc0fdc63391b568e4cbcf289300e295dc Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 18 Aug 2015 22:06:28 -0400
Subject: [PATCH] fix bug 605

---
 src/expr/type_node.cpp            |  2 ++
 test/regress/regress0/Makefile.am |  1 +
 test/regress/regress0/bug605.cvc  | 30 ++++++++++++++++++++++++++++++
 3 files changed, 33 insertions(+)
 create mode 100644 test/regress/regress0/bug605.cvc

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 1f2963e18..5319e1e98 100644
--- 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 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
-- 
2.30.2