added options for controlling resource step-count for various solving stages

2 files changed, 4 insertions, 4 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 6d32120d9..37fea2c67 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -170,13 +170,13 @@ uint64_t ResourceManager::getTimeRemaining() const {
   return d_thisCallTimeBudget - time_passed;
 }
 
-void ResourceManager::spendResource() throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(uint64_t ammount) throw (UnsafeInterruptException) {
   ++d_spendResourceCalls;
-  ++d_cumulativeResourceUsed;
+  d_cumulativeResourceUsed += ammount;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  ++d_thisCallResourceUsed;
+  d_thisCallResourceUsed += ammount;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
 	Trace("limit") << "                 on call " << d_spendResourceCalls << std::endl;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index d1ec0456a..9c2812f0f 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -128,7 +128,7 @@ public:
     return d_thisCallResourceBudget;
   }
 
-  void spendResource() throw(UnsafeInterruptException);
+  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
 
   void setHardLimit(bool value);
   void setResourceLimit(uint64_t units, bool cumulative = false);