1 files changed, 8 insertions, 4 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 70e0b9157..f71dac3e5 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -23,9 +23,10 @@
 #include "context/cdo.h"
 #include "proof/clause_id.h"
 #include "proof/resolution_bitvector_proof.h"
+#include "prop/bv_sat_solver_notify.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 #include "prop/sat_solver.h"
-#include "prop/bv_sat_solver_notify.h"
+#include "util/resource_manager.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,11 +47,14 @@ class BVMinisatSatSolver : public BVSatSolverInterface,
       return d_notify->notify(toSatLiteral(lit));
     }
     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
-    void spendResource(unsigned amount) override
+    void spendResource(ResourceManager::Resource r) override
+    {
+      d_notify->spendResource(r);
+    }
+    void safePoint(ResourceManager::Resource r) override
     {
-      d_notify->spendResource(amount);
+      d_notify->safePoint(r);
     }
-    void safePoint(unsigned amount) override { d_notify->safePoint(amount); }
   };
 
 	std::unique_ptr<BVMinisat::SimpSolver> d_minisat;