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.cpp | |
| parent | f1c8b8cda3b99353adbe424e0bf1259147001f3c (diff) | |
Fixes for issue 1404 (#1409)
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 65810109c..02dd92ad7 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -302,7 +302,8 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ } /** add term */ -void TheoryModel::addTerm(TNode n ){ +void TheoryModel::addTermInternal(TNode n) +{ Assert(d_equalityEngine->hasTerm(n)); Trace("model-builder-debug2") << "TheoryModel::addTerm : " << n << std::endl; //must collect UF terms @@ -512,6 +513,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { if( options::ufHo() ){ Trace("model-builder-debug") << " ...function is first-class member of equality engine" << std::endl; + Assert(d_equalityEngine->hasTerm(f)); // assign to representative if higher-order Node r = d_equalityEngine->getRepresentative( f ); //always replace the representative, since it is initially assigned to itself |