diff options
Diffstat (limited to 'src/theory/bv/bitblast/bitblaster.h')
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 4 |
1 files changed, 2 insertions, 2 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 {} |