3 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 82921b3a0..defc66b74 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -27,12 +27,12 @@
 #include "proof/bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "prop/sat_solver_types.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
 #include "theory/theory_registrar.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
-
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -111,7 +111,7 @@ class MinisatEmptyNotify : public prop::BVSatSolverNotify
   void notify(prop::SatClause& clause) override {}
   void spendResource(ResourceManager::Resource r) override
   {
-    NodeManager::currentResourceManager()->spendResource(r);
+    smt::currentResourceManager()->spendResource(r);
   }
 
   void safePoint(ResourceManager::Resource r) override {}
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index ef583cc13..4acd1d2f8 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -67,7 +67,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
     default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
-  ResourceManager* rm = NodeManager::currentResourceManager();
+  ResourceManager* rm = smt::currentResourceManager();
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_bitblastingRegistrar.get(),
                                                d_nullContext.get(),
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 9abeee65e..c3a305952 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -79,7 +79,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
 
-  ResourceManager* rm = NodeManager::currentResourceManager();
+  ResourceManager* rm = smt::currentResourceManager();
   d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
                                                d_nullRegistrar.get(),
                                                d_nullContext.get(),
@@ -581,7 +581,7 @@ void TLazyBitblaster::clearSolver() {
   // recreate sat solver
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
-  ResourceManager* rm = NodeManager::currentResourceManager();
+  ResourceManager* rm = smt::currentResourceManager();
   d_cnfStream.reset(new prop::TseitinCnfStream(
       d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm));
   d_satSolverNotify.reset(