1 files changed, 21 insertions, 14 deletions

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index d0b299d3b..12d415cad 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -2,9 +2,9 @@
 /*! \file bv_inequality_graph.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Paul Meng, Morgan Deters
+ **   Liana Hadarean, Aina Niemetz, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -415,15 +415,17 @@ void InequalityGraph::backtrack() {
   }
 }
 
-Node InequalityGraph::makeDiseqSplitLemma(TNode diseq) {
-  Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+Node InequalityGraph::makeDiseqSplitLemma(TNode diseq)
+{
+  Assert(diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL);
+  NodeManager* nm = NodeManager::currentNM();
   TNode a = diseq[0][0];
   TNode b = diseq[0][1];
-  Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
-  Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);
-  Node eq = diseq[0]; 
-  Node lemma = utils::mkNode(kind::OR, a_lt_b, b_lt_a, eq);
-  return lemma; 
+  Node a_lt_b = nm->mkNode(kind::BITVECTOR_ULT, a, b);
+  Node b_lt_a = nm->mkNode(kind::BITVECTOR_ULT, b, a);
+  Node eq = diseq[0];
+  Node lemma = nm->mkNode(kind::OR, a_lt_b, b_lt_a, eq);
+  return lemma;
 }
 
 void InequalityGraph::checkDisequalities(std::vector<Node>& lemmas) {
@@ -460,14 +462,19 @@ BitVector InequalityGraph::getValueInModel(TNode node) const {
   return getValue(id); 
 }
 
-void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) {
-  for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
+void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  for (ModelValues::const_iterator it = d_modelValues.begin();
+       it != d_modelValues.end();
+       ++it)
+  {
     TermId id = (*it).first;
     BitVector value = (*it).second.value;
     TNode var = getTermNode(id);
     Node constant = utils::mkConst(value);
-    Node assignment = utils::mkNode(kind::EQUAL, var, constant);
-    assignments.push_back(assignment); 
-    Debug("bitvector-model") << "   " << var <<" => " << constant << "\n"; 
+    Node assignment = nm->mkNode(kind::EQUAL, var, constant);
+    assignments.push_back(assignment);
+    Debug("bitvector-model") << "   " << var << " => " << constant << "\n";
   }
 }