Resource-limiting work.

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

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d0b99f869..c86572ead 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -103,8 +103,11 @@ void BitblastSolver::bitblastQueue() {
       // don't bit-blast lemma atoms
       continue;
     }
-    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; 
-    d_bitblaster->bbAtom(atom);
+    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
+    {
+      TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
+      d_bitblaster->bbAtom(atom);
+    }
   }
 }
 
@@ -149,6 +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();
     bool ok = d_bitblaster->propagate();
     if (!ok) {
       std::vector<TNode> conflictAtoms;