added number of resource units used as a stat

2 files changed, 2 insertions, 2 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index b0fd37fd2..7aeb2fc0f 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -172,10 +172,10 @@ unsigned long ResourceManager::getTimeRemaining() const {
 
 void ResourceManager::spendResource() throw (UnsafeInterruptException) {
   ++d_spendResourceCalls;
+  ++d_cumulativeResourceUsed;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  ++d_cumulativeResourceUsed;
   ++d_thisCallResourceUsed;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index a16f60910..94e7dbba2 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -150,7 +150,7 @@ public:
   void endCall();
 
   static unsigned long getFrequencyCount() { return s_resourceCount; }
-
+  friend class SmtEngine;
 };/* class ResourceManager */
 
 }/* CVC4 namespace */