From a5c5c2f8db7340ceaa3628575ff0e672370374cc Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 27 Mar 2013 20:34:18 -0400 Subject: [PATCH] Added assertion --- src/theory/bv/bitblaster.cpp | 8 +++----- 1 file 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]; -- 2.30.2