9 files changed, 20 insertions, 18 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index d4d7bc04c..4d953b03c 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -135,8 +135,8 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
-    void spendResource();
-    void safePoint();
+    void spendResource(uint64_t ammount);
+    void safePoint(uint64_t ammount);
   };
   
   TheoryBV *d_bv;
@@ -240,10 +240,10 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
-  void spendResource() {
-    NodeManager::currentResourceManager()->spendResource();
+  void spendResource(uint64_t ammount) {
+    NodeManager::currentResourceManager()->spendResource(ammount);
   }
-  void safePoint() {}
+  void safePoint(uint64_t ammount) {}
 };
 
 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 57a635c20..0c087ddb9 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -67,7 +67,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
-  d_bv->spendResource();
+  d_bv->spendResource(1);
   Assert (isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
   d_assertionSet.insert(formula);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index c86572ead..7e3ed46c8 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -152,7 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) {
 
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation) {
-    d_bv->spendResource();
+    d_bv->spendResource(1);
     bool ok = d_bitblaster->propagate();
     if (!ok) {
       std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 9481b9894..13c31463b 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/slicer.h"
 #include "theory/theory_model.h"
 #include "theory/bv/options.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -167,7 +168,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::theoryCheckStep());
 
   d_checkCalled = true; 
   Assert (!d_bv->inConflict());
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 660551fe2..55dcbb03a 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -18,6 +18,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -29,7 +30,7 @@ using namespace CVC4::theory::bv::utils;
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   ++(d_statistics.d_numCallstoCheck);
-  d_bv->spendResource();
+  d_bv->spendResource(options::theoryCheckStep());
 
   bool ok = true;
   while (!done() && ok) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 065d5d5ef..eca9f12ab 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -103,7 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::bitblastStep());
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 
   d_termBBStrategies[node.getKind()] (node, bits, this);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 080f23143..61472fd79 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -170,7 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::bitblastStep());
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -356,12 +356,12 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource() {
-  d_bv->spendResource();
+void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) {
+  d_bv->spendResource(ammount);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint() {
-  d_bv->d_out->safePoint();
+void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) {
+  d_bv->d_out->safePoint(ammount);
 }
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 9dcd5ac62..6f399cb7a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,8 +107,8 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
-void TheoryBV::spendResource() throw(UnsafeInterruptException) {
-  getOutputChannel().spendResource();
+void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+  getOutputChannel().spendResource(ammount);
 }
 
 TheoryBV::Statistics::Statistics():
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 11d8cb895..3317d1b01 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,7 +103,7 @@ private:
 
   Statistics d_statistics;
 
-  void spendResource() throw(UnsafeInterruptException);
+  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero