1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index bb4b480d6..6248782bd 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -40,7 +40,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
-    d_slicer(),
+    d_slicer(c),
     d_bitblastAssertionsQueue(c),
     d_bitblastSolver(c, this),
     d_coreSolver(c, this, &d_slicer),
@@ -74,6 +74,8 @@ TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_solveTimer);
 }
 
+
+
 void TheoryBV::preRegisterTerm(TNode node) {
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
@@ -81,10 +83,6 @@ void TheoryBV::preRegisterTerm(TNode node) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
-
-  if (node.getKind() == kind::EQUAL) {
-    d_slicer.processEquality(node); 
-  }
   
   d_bitblastSolver.preRegister(node);
   d_coreSolver.preRegister(node);