diff options
Diffstat (limited to 'src/theory/fp/theory_fp.cpp')
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 4c59b1c06..5eb9e576d 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -1023,7 +1023,8 @@ bool TheoryFp::collectModelInfo(TheoryModel* m) { std::set<Node> relevantTerms; // Work out which variables are needed - computeRelevantTerms(relevantTerms); + const std::set<Kind>& irrKinds = m->getIrrelevantKinds(); + computeAssertedTerms(relevantTerms, irrKinds); // this override behavior to not assert equality engine return collectModelValues(m, relevantTerms); } |