From 408855d37c90c701508b5207cb3588e09cc12583 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 23 Oct 2012 19:46:55 +0000 Subject: [PATCH] fixed TheoryBV collectModel info to check for shared terms; this seems to fix bug424 --- src/theory/bv/bitblast_strategies.cpp | 6 +----- 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::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); + } } } -- 2.30.2