Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

1 files changed, 7 insertions, 0 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index ad187aa46..8d7b014cc 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -30,6 +30,7 @@
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
 #include "prop/minisat/minisat.h"
+#include "smt/smt_engine_scope.h"
 #include <queue>
 
 using namespace std;
@@ -665,6 +666,12 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
+  if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
+    NodeManager::currentResourceManager()->spendResource();
+    d_convertAndAssertCounter = 0;
+  }
+  ++d_convertAndAssertCounter;
+
   switch(node.getKind()) {
   case AND:
     convertAndAssertAnd(node, negated);