From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 23 Oct 2012 19:46:55 +0000 (+0000)
Subject: fixed TheoryBV collectModel info to check for shared terms; this seems to fix bug424
X-Git-Tag: cvc5-1.0.0~7686
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=408855d37c90c701508b5207cb3588e09cc12583;p=cvc5.git

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 5d0ef8aa5..d2fbb432b 100644
--- 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 593189e56..41d98326e 100644
--- 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); 
+    }
   }
 }