From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 28 Mar 2013 00:34:18 +0000 (-0400)
Subject: Added assertion
X-Git-Tag: cvc5-1.0.0~7361^2~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5c5c2f8db7340ceaa3628575ff0e672370374cc;p=cvc5.git

Added assertion
---

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];