1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/model.h b/src/theory/model.h
index acfcb4849..5581ce777 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -174,7 +174,7 @@ private:
     return (*it).second;
   }
 
-  Node nextTypeEnum(TypeNode t)
+  Node nextTypeEnum(TypeNode t, bool useBaseType = false)
   {
     TypeEnumerator* te;
     TypeToTypeEnumMap::iterator it = d_teMap.find(t);
@@ -189,6 +189,9 @@ private:
       return Node();
     }
 
+    if (useBaseType) {
+      t = t.getBaseType();
+    }
     iterator itSet = d_typeSet.find(t);
     std::set<Node>* s;
     if (itSet == d_typeSet.end()) {