From 390477967f6179b03754c27be027b22ea77052bc Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 26 Mar 2011 22:26:06 +0000
Subject: fix for bug 253, was propagating an asserted literal also fixing some
 compile warnings in attributes

---
 src/theory/bv/theory_bv.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'src/theory/bv')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e106f3b84..bcf6339ac 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -56,11 +56,18 @@ void TheoryBV::check(Effort e) {
 
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
-  while(!done()) {
-
+  // Get all the assertions
+  std::vector<TNode> assertionsList;
+  while (!done()) {
     // Get the assertion
     TNode assertion = get();
     d_assertions.insert(assertion);
+    assertionsList.push_back(assertion);
+  }
+
+  for (unsigned i = 0; i < assertionsList.size(); ++ i) {
+
+    TNode assertion = assertionsList[i];
 
     BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl;
 
-- 
cgit v1.2.3