diff options
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 5 |
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()) { |