fix for bug 253, was propagating an asserted literal

also fixing some compile warnings in attributes

diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 3bbab17a42c9297256100de34bbebe4846ce6d94..cdb5735c3cd5bc8645643cd66e4dd3e539d66ca0 100644 (file)
--- 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 e106f3b8401df7d41d3479233123d7f923204fcb..bcf6339acb3e17e5991979f475e01386a75862c1 100644 (file)
--- 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;
 

diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index 15c2f699f0827633b3e5a9480a9a19407a3b0daa..f1a12e165fe8def3abd478541f26a77fe704c193 100644 (file)
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -67,9 +67,7 @@ TESTS =       \
        a78test0002.smt \
        a95test0002.smt \
        bitvec0.smt \
-       bitvec2.smt
-
-EXTRA_DIST = $(TESTS) \
+       bitvec2.smt \
        bitvec3.smt \
        bitvec5.smt