From 60f6d09d7ad9e37f5a23e6a2b0e47a7b0e47df81 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Thu, 20 Aug 2015 17:21:50 +0100
Subject: [PATCH] fix to bug659 due to algebraic solver model building

---
 src/theory/bv/bv_subtheory_algebraic.cpp |  7 +++++--
 src/theory/bv/theory_bv_utils.cpp        | 15 +++++++++++++++
 src/theory/bv/theory_bv_utils.h          |  2 ++
 3 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 96b205bb1..e6e3120f5 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -684,16 +684,19 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     }
   }
 
+  NodeSet leaf_vars;
   Debug("bitvector-model") << "Substitutions:\n";
   for (unsigned i = 0; i < variables.size(); ++i) {
     TNode current = variables[i];
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "   " << current << " => " << subst << "\n";
     values[i] = subst;
+    utils::collectVariables(subst, leaf_vars);
   }
 
   Debug("bitvector-model") << "Model:\n";
-  for (BVQuickCheck::vars_iterator it = d_quickSolver->beginVars(); it != d_quickSolver->endVars(); ++it) {
+
+  for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
     TNode var = *it;
     Node value = d_quickSolver->getVarValue(var, true);
     Assert (!value.isNull() || !fullModel);
@@ -712,7 +715,7 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n"; 
     // Doesn't have to be constant as it may be irrelevant
-    // Assert (subst.getKind() == kind::CONST_BITVECTOR); 
+    Assert (subst.getKind() == kind::CONST_BITVECTOR); 
     model->assertEquality(variables[i], subst, true);
   }
 
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 824dc5b92..d2025b1b8 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -100,3 +100,18 @@ uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) {
   seen.insert(node);
   return size;
 }
+
+
+
+void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) {
+  if (vars.find(node) != vars.end())
+    return;
+
+  if (Theory::isLeafOf(node, THEORY_BV) && node.getKind() != kind::CONST_BITVECTOR) {
+    vars.insert(node);
+    return;
+  }
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    collectVariables(node[i], vars);
+  }
+}
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index a8b6887e5..ba8074fbb 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -513,6 +513,8 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 
 uint64_t numNodes(TNode node, NodeSet& seen);
 
+void collectVariables(TNode node, NodeSet& vars);
+
 }
 }
 }
-- 
2.30.2