diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-10-19 18:38:54 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-10-19 18:38:54 +0000 |
commit | 6f8d2ea6e8b6a8ff43352740131486bee6b2da27 (patch) | |
tree | 2573711d03d528df6dfce01099712e1cb4b05ab9 /src/theory/bv/bitblast_strategies.cpp | |
parent | 28af31bf1efff6fc143da3a9db9996162c2befab (diff) |
BV theory model fix
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index a6cd0af29..5d0ef8aa5 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -345,9 +345,11 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; BVDebug("bitvector-bb") << " with bits " << toString(bits); } - // this is not necessairily a variable, but it is a term the theory of bitvectors treads as one - // e.g. a select over a bv array - bb->storeVariable(node); + + if (Theory::theoryOf(node) == theory::THEORY_BV || + bb->isSharedTerm(node)) { + bb->storeVariable(node); + } } |