Fixed bug in model builder with subtypes

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index b67140db8..33f6ca9c8 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -552,7 +552,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
     else if (!rep.isNull()) {
       assertedReps[eqc] = rep;
       typeRepSet.add(eqct.getBaseType(), eqc);
-      allTypes.insert(eqct);
+      allTypes.insert(eqct.getBaseType());
     }
     else {
       typeNoRepSet.add(eqct, eqc);
@@ -642,7 +642,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
             Trace("model-builder") << "    Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
             if (normalized.isConst()) {
               changed = true;
-              typeConstSet.add(t.getBaseType(), normalized);
+              typeConstSet.add(tb, normalized);
               constantReps[*i] = normalized;
               assertedReps.erase(*i);
               i2 = i;