Fixes for issue 1404 (#1409)

1 files changed, 5 insertions, 6 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index b08c8f1ca..ac12b37e3 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -350,11 +350,10 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   }
   // AJR: build ordered list of types that ensures that base types are
   // enumerated first.
-  //   (I think) this is only strictly necessary for finite model finding +
-  //   parametric types
-  //   instantiated with uninterpreted sorts, but is probably a good idea to do
-  //   in general
-  //   since it leads to models with smaller term sizes.
+  // (I think) this is only strictly necessary for finite model finding +
+  // parametric types instantiated with uninterpreted sorts, but is probably
+  // a good idea to do in general since it leads to models with smaller term
+  // sizes.
   std::vector<TypeNode> type_list;
   eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
   for (; !eqcs_i.isFinished(); ++eqcs_i)
@@ -396,7 +395,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
                                << std::endl;
       }
       // model-specific processing of the term
-      tm->addTerm(n);
+      tm->addTermInternal(n);
     }
 
     // Assign representative for this EC