Updates to model-based array solver

Minor fixes to bv and theory_engine

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 9a52a05a5..feca721c9 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -412,8 +412,11 @@ bool Bitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
 }
 
-bool Bitblaster::hasValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+Node Bitblaster::getVarValue(TNode a) {
+  if (d_termCache.find(a) == d_termCache.end()) {
+    Assert(isSharedTerm(a));
+    return Node();
+  }
   Bits bits = d_termCache[a];
   for (int i = bits.size() -1; i >= 0; --i) {
     SatValue bit_value;