From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 8 Nov 2014 00:40:54 +0000 (-0800)
Subject: Fixed bug in model builder with subtypes
X-Git-Tag: cvc5-1.0.0~6513
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e5de3b175640a5592b668dd18496be5a29405c5b;p=cvc5.git

Fixed bug in model builder with subtypes
---

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;