diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 13:18:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-20 13:18:11 -0500 |
commit | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (patch) | |
tree | c50d4bbb5cfeee385b2f5d1bf8e5b9281def3859 /src/theory/theory_model.cpp | |
parent | ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 (diff) |
Do not assign higher-order representative if function does not exist (#4073)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index bf0a82a20..7bfb0e8f3 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -669,8 +669,8 @@ bool TheoryModel::areFunctionValuesEnabled() const } void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { - Assert(d_uf_models.find(f) == d_uf_models.end()); Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; + Assert(d_uf_models.find(f) == d_uf_models.end()); if( options::ufHo() ){ //we must rewrite the function value since the definition needs to be a constant value @@ -685,9 +685,9 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { d_uf_models[f] = f_def; } - if( options::ufHo() ){ + if (options::ufHo() && d_equalityEngine->hasTerm(f)) + { 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 |