summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast_strategies.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast_strategies.cpp')
-rw-r--r--src/theory/bv/bitblast_strategies.cpp6
1 files changed, 1 insertions, 5 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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback