From 03930f2a6fdfb85ecc81594ec65f41d7c1284577 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 15 May 2012 22:02:47 +0000
Subject: [PATCH] fixed QF_BV performance problem due to using CDList instead
 of CDQueue

---
 src/theory/bv/theory_bv.cpp | 7 ++++---
 src/theory/bv/theory_bv.h   | 2 +-
 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;
-- 
2.30.2