diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-10-23 19:46:55 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-10-23 19:46:55 +0000 |
commit | 408855d37c90c701508b5207cb3588e09cc12583 (patch) | |
tree | abf2c8e9b2c1a0578a7d607cbe4e645cbc46b633 /src | |
parent | 5e64d60e49db9176c310f15cb206e3fda3e31973 (diff) |
fixed TheoryBV collectModel info to check for shared terms; this seems to fix bug424
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblaster.cpp | 6 |
2 files changed, 5 insertions, 7 deletions
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); + } } } |