fixed QF_BV performance problem due to using CDList instead of CDQueue

2 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d005e9473..445b2d242 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -205,9 +205,10 @@ void TheoryBV::check(Effort e)
 
   // bit-blasting atoms on queue
 
-  for (unsigned i = 0; i < d_bitblastQueue.size(); ++i) {
-    d_bitblaster->bbAtom(d_bitblastQueue[i]);
-    // would be nice to clear the bitblastQueue?
+  while (!d_bitblastQueue.empty()) {
+    TNode node = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(node);
+    d_bitblastQueue.pop(); 
   }
   
   // bit-blaster propagation 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 6ef9d18dd..9ab5f8e1c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -56,7 +56,7 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
 
-  context::CDList<TNode> d_bitblastQueue; 
+  context::CDQueue<TNode> d_bitblastQueue; 
   
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;