diff options
| -rw-r--r-- | src/theory/bv/bitblaster.cpp | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index feca721c9..d3a54a3e4 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -412,11 +412,8 @@ bool Bitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } -Node Bitblaster::getVarValue(TNode a) { - if (d_termCache.find(a) == d_termCache.end()) { - Assert(isSharedTerm(a)); - return Node(); - } +bool Bitblaster::hasValue(TNode a) { + Assert (d_termCache.find(a) != d_termCache.end()); Bits bits = d_termCache[a]; for (int i = bits.size() -1; i >= 0; --i) { SatValue bit_value; @@ -441,6 +438,7 @@ Node Bitblaster::getVarValue(TNode a) { */ Node Bitblaster::getVarValue(TNode a) { if (d_termCache.find(a) == d_termCache.end()) { + Assert(isSharedTerm(a)); return Node(); } Bits bits = d_termCache[a]; |