summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast/bitblaster.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast/bitblaster.h')
-rw-r--r--src/theory/bv/bitblast/bitblaster.h4
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 {}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback