fixed TheoryBV collectModel info to check for shared terms; this seems to fix bug424

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 5d0ef8aa516c01723611fe50a7d60cffc45a7f95..d2fbb432b1f038c6450c8f32b74aa8a94f868a39 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -346,11 +346,7 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
-    if (Theory::theoryOf(node) == theory::THEORY_BV ||
-        bb->isSharedTerm(node)) {
-    bb->storeVariable(node);
-    }
-
+   bb->storeVariable(node);
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 593189e5672ac2ff2348e211587e816d9f457adb..41d98326e631b22f0a89e1da91b0bafbd8de6214 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -427,8 +427,10 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    Node const_value = getVarValue(var);
-    m->assertEquality(var, const_value, true); 
+    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
+      Node const_value = getVarValue(var);
+      m->assertEquality(var, const_value, true); 
+    }
   }
 }