1 files changed, 23 insertions, 25 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 0a4499c11..ced320d92 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -113,13 +113,31 @@ TheoryBV::TheoryBV(context::Context* c,
 
 TheoryBV::~TheoryBV() {}
 
-void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
+
+bool TheoryBV::needsEqualityEngine(EeSetupInfo& esi)
+{
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
   {
-    return;
+    return core->needsEqualityEngine(esi);
   }
-  if (options::bitvectorEqualitySolver()) {
-    dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
+  // otherwise we don't use an equality engine
+  return false;
+}
+
+void TheoryBV::finishInit()
+{
+  // these kinds are semi-evaluated in getModelValue (applications of this
+  // kind are treated as variables)
+  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+  d_valuation.setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if (core)
+  {
+    // must finish initialization in the core solver
+    core->finishInit();
   }
 }
 
@@ -185,16 +203,6 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
   Unreachable();
 }
 
-void TheoryBV::finishInit()
-{
-  // these kinds are semi-evaluated in getModelValue (applications of this
-  // kind are treated as variables)
-  TheoryModel* tm = d_valuation.getModel();
-  Assert(tm != nullptr);
-  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
-  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
-}
-
 TrustNode TheoryBV::expandDefinition(Node node)
 {
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
@@ -582,16 +590,6 @@ void TheoryBV::propagate(Effort e) {
   }
 }
 
-
-eq::EqualityEngine * TheoryBV::getEqualityEngine() {
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if( core ){
-    return core->getEqualityEngine();
-  }else{
-    return NULL;
-  }
-}
-
 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
   eq::EqualityEngine * ee = getEqualityEngine();
   if( ee ){