1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b74506e4d..e5b5ed664 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -170,6 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
+  d_bv->spendResource();
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -355,6 +356,10 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
+void TLazyBitblaster::MinisatNotify::spendResource() {
+  d_bv->spendResource();
+}
+
 void TLazyBitblaster::MinisatNotify::safePoint() {
   d_bv->d_out->safePoint();
 }