fixed some model stuff

5 files changed, 28 insertions, 6 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 773685997..a952b2929 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -346,7 +346,7 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
-  bb->storeVariable(node);
+   bb->storeVariable(node);
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 6da3b8efc..9a52a05a5 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -428,9 +428,18 @@ bool Bitblaster::hasValue(TNode a) {
   }
   return true; 
 }
-
+/** 
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned. 
+ * 
+ * @param a 
+ * 
+ * @return 
+ */
 Node Bitblaster::getVarValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+  if (d_termCache.find(a) == d_termCache.end()) {
+    return Node(); 
+  }
   Bits bits = d_termCache[a];
   Integer value(0); 
   for (int i = bits.size() -1; i >= 0; --i) {
@@ -455,6 +464,10 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
       Node const_value = getVarValue(var);
+      if(const_value == Node()) {
+        // if the value is unassigned just set it to zero
+        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+      }
       Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                 << var << " "
                                 << const_value << "))\n";
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 9c4a5c5b6..30eaaa764 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -141,5 +141,7 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node BitblastSolver::getModelValue(TNode node) {
-  return d_bitblaster->getVarValue(node);
+  Node val = d_bitblaster->getVarValue(node);
+  Assert (val != Node() || d_bv->isSharedTerm(node));
+  return val; 
 }
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c4f1b1b86..91fed8a67 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -407,7 +407,11 @@ Node CoreSolver::getModelValue(TNode var) {
   if (repr.getKind() == kind::CONST_BITVECTOR) {
     return repr; 
   }
-  Assert (d_modelValues.find(repr) != d_modelValues.end()); 
+  if (d_modelValues.find(repr) == d_modelValues.end()) {
+    // it may be a shared term that never gets asserted
+    Assert(d_bv->isSharedTerm(var));
+    return Node(); 
+  }
   return d_modelValues[repr]; 
 }
 
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 9f7760608..5504dbc11 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -181,7 +181,10 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) {
 
 Node InequalitySolver::getModelValue(TNode var) {
   Assert (isComplete());
-  Assert (d_inequalityGraph.hasValueInModel(var)); 
+  if (!d_inequalityGraph.hasValueInModel(var)) {
+    Assert (d_bv->isSharedTerm(var));
+    return Node(); 
+  }
   BitVector val = d_inequalityGraph.getValueInModel(var);
   return utils::mkConst(val); 
 }