fix for bug 253, was propagating an asserted literal

also fixing some compile warnings in attributes

2 files changed, 13 insertions, 6 deletions

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 3bbab17a4..cdb5735c3 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -411,7 +411,7 @@ class CDAttrHash<bool> :
       d_key(key),
       d_word(word),
       d_bit(bit) {
-      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor(%p, %p, %lx, %u)\n", &map, key, word, bit);
+      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor(%p, %p, %llx, %u)\n", &map, key, word, bit);
     }
 
     BitAccessor& operator=(bool b) {
@@ -419,19 +419,19 @@ class CDAttrHash<bool> :
         // set the bit
         d_word |= (1 << d_bit);
         d_map.insert(d_key, d_word);
-        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::set(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::set(%p, %p, %llx, %u)\n", &d_map, d_key, d_word, d_bit);
       } else {
         // clear the bit
         d_word &= ~(1 << d_bit);
         d_map.insert(d_key, d_word);
-        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+        Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %llx, %u)\n", &d_map, d_key, d_word, d_bit);
       }
 
       return *this;
     }
 
     operator bool() const {
-      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit);
+      Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %llx, %u)\n", &d_map, d_key, d_word, d_bit);
       return (d_word & (1 << d_bit)) ? true : false;
     }
   };/* class CDAttrHash<bool>::BitAccessor */
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;