5 files changed, 16 insertions, 19 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 66eea0997..9c6c4af9b 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -26,7 +26,6 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
-#include "smt/smt_globals.h"
 #include "theory/theory_registrar.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 2e4f06c38..dd561667c 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -43,16 +43,13 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv)
   d_bitblastingRegistrar = new BitblastingRegistrar(this);
   d_nullContext = new context::Context();
 
-  d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext,
-                                                      smtStatisticsRegistry(),
-                                                      "EagerBitblaster");
-  d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
-                                           d_bitblastingRegistrar,
-                                           d_nullContext,
-                                           d_bv->globals(),
-                                           options::proof(),
-                                           "EagerBitblaster");
-  
+  d_satSolver = prop::SatSolverFactory::createMinisat(
+      d_nullContext, smtStatisticsRegistry(), "EagerBitblaster");
+
+  d_cnfStream = new prop::TseitinCnfStream(
+      d_satSolver, d_bitblastingRegistrar, d_nullContext, options::proof(),
+      "EagerBitblaster");
+
   MinisatEmptyNotify* notify = new MinisatEmptyNotify();
   d_satSolver->setNotify(notify);
   d_bvp = NULL;
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 9268e2152..ca21e98c4 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -56,13 +56,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv,
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
                                            d_nullRegistrar,
                                            d_nullContext,
-                                           d_bv->globals(),
                                            options::proof(),
                                            "LazyBitblaster");
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
+    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv,
+                                                            this);
 
   d_satSolver->setNotify(d_satSolverNotify);
 }
@@ -526,11 +526,12 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver = prop::SatSolverFactory::createMinisat(
       d_ctx, smtStatisticsRegistry());
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_nullRegistrar,
-                                           d_nullContext, d_bv->globals());
+                                           d_nullContext);
 
   d_satSolverNotify = d_emptyNotify ?
     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
-    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
+    (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv,
+                                                            this);
   d_satSolver->setNotify(d_satSolverNotify);
 }
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 8f7e975cd..191f70638 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -44,8 +44,8 @@ namespace bv {
 
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, globals),
+                   const LogicInfo& logicInfo)
+    : Theory(THEORY_BV, c, u, out, valuation, logicInfo),
       d_context(c),
       d_alreadyPropagatedSet(c),
       d_sharedTermsSet(c),
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 27138abfc..1da15abf8 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -22,7 +22,6 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
-#include "smt/smt_globals.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
@@ -56,7 +55,8 @@ class TheoryBV : public Theory {
 
 public:
 
-  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals);
+  TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out,
+           Valuation valuation, const LogicInfo& logicInfo);
 
   ~TheoryBV();