1 files changed, 15 insertions, 17 deletions
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 237b04172..d8a784544 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -54,7 +54,11 @@ void BitblastSolver::preRegister(TNode node) {
        node.getKind() == kind::BITVECTOR_SLT ||
        node.getKind() == kind::BITVECTOR_SLE) &&
       !d_bitblaster->hasBBAtom(node)) {
-    d_bitblastQueue.push_back(node);
+    if (options::bitvectorEagerBitblast()) {
+      d_bitblaster->bbAtom(node);
+    } else {
+      d_bitblastQueue.push_back(node);
+    }
   }
 }
 
@@ -62,29 +66,23 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
   d_bitblaster->explain(literal, assumptions);
 }
 
+void BitblastSolver::bitblastQueue() {
+  while (!d_bitblastQueue.empty()) {
+    TNode atom = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(atom);
+    d_bitblastQueue.pop();
+  }
+}
 
 bool BitblastSolver::check(Theory::Effort e) {
   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; 
+  Assert(!options::bitvectorEagerBitblast());
+
   ++(d_statistics.d_numCallstoCheck); 
-  //// Eager bit-blasting
-  if (options::bitvectorEagerBitblast()) {
-    while (!done()) {
-      TNode assertion = get(); 
-      TNode atom = assertion.getKind() == kind::NOT ? assertion[0] : assertion;
-      if (atom.getKind() != kind::BITVECTOR_BITOF) {
-        d_bitblaster->bbAtom(atom);
-      }
-      return true;
-    }
-  }
 
   //// Lazy bit-blasting
   // bit-blast enqueued nodes
-  while (!d_bitblastQueue.empty()) {
-    TNode atom = d_bitblastQueue.front();
-    d_bitblaster->bbAtom(atom);
-    d_bitblastQueue.pop();
-  }
+  bitblastQueue();
 
   // Processing assertions  
   while (!done()) {