summaryrefslogtreecommitdiff
path: root/src/theory/sep/theory_sep.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sep/theory_sep.cpp')
-rw-r--r--src/theory/sep/theory_sep.cpp7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 81afc0da2..4f31f10b5 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -201,8 +201,13 @@ void TheorySep::computeCareGraph() {
void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){
+ set<Node> termSet;
+
+ // Compute terms appearing in assertions and shared terms
+ computeRelevantTerms(termSet);
+
// Send the equality engine information to the model
- m->assertEqualityEngine( &d_equalityEngine );
+ m->assertEqualityEngine( &d_equalityEngine, &termSet );
}
void TheorySep::postProcessModel( TheoryModel* m ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback