started work on the inequality bv subtheory

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 5d034287d..ed1ba40a8 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -40,15 +40,16 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
-    d_slicer(c),
     d_bitblastSolver(c, this),
-    d_coreSolver(c, this, &d_slicer),
+    d_coreSolver(c, this),
     d_statistics(),
     d_conflict(c, false),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
-  {}
+  {
+    
+  }
 
 TheoryBV::~TheoryBV() {}
 
@@ -289,7 +290,6 @@ void TheoryBV::addSharedTerm(TNode t) {
 }
 
 
-
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitvectorEagerBitblast()) {