1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index e809a2566..f8e6882a9 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -174,5 +174,7 @@ void EqualitySolver::collectModelInfo(TheoryModel* m) {
                                << *it << ")\n";
     }
   }
-  m->assertEqualityEngine(&d_equalityEngine);
+  set<Node> termSet;
+  d_bv->computeRelevantTerms(termSet);
+  m->assertEqualityEngine(&d_equalityEngine, &termSet);
 }