From 93a162548e1df0102936deae560b873b7f143bf4 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 8 Nov 2012 12:22:06 +0000
Subject: Fixed two small bugs in model generation

---
 src/theory/model.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src/theory/model.h')

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()) {
-- 
cgit v1.2.3