diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-27 20:34:18 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-27 20:34:30 -0400 |
commit | a5c5c2f8db7340ceaa3628575ff0e672370374cc (patch) | |
tree | 45afde09b97c564bb58b6ed011faafe3dcdd32f0 /src/theory/bv | |
parent | ba03942a69a80ac93217e17b076673a522e50680 (diff) |
Added assertion
Diffstat (limited to 'src/theory/bv')
-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]; |