diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-08 12:22:06 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-08 12:22:06 +0000 |
| commit | 93a162548e1df0102936deae560b873b7f143bf4 (patch) | |
| tree | d51d7b24498743ac15ffe1eecabe7bb1a0ceb17d /src/theory/model.h | |
| parent | 8115182a602848ee7d233b0e4f197289be4fef3c (diff) | |
Fixed two small bugs in model generation
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()) { |