diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-30 09:57:06 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 09:57:06 -0600 |
commit | 89b6c052e96cc907800650de93d2f238e19acd38 (patch) | |
tree | a634adc60388ab164d707511be0f1f52e75aef61 /src/theory/theory_model_builder.cpp | |
parent | f1c8b8cda3b99353adbe424e0bf1259147001f3c (diff) |
Fixes for issue 1404 (#1409)
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 11 |
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 |