Prevent ref count from reaching zero in BV instantiator (#3512)

4 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index eacc3032c..c7aaf572c 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -384,7 +384,7 @@ Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci,
   std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited;
   visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>());
   // whether the visited term contains pv
-  std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv;
+  std::unordered_map<Node, bool, NodeHashFunction> visited_contains_pv;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs;
   std::stack<std::stack<TNode> > visit;
@@ -534,7 +534,7 @@ Node BvInstantiator::rewriteTermForSolvePv(
     Node pv,
     Node n,
     std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   NodeManager* nm = NodeManager::currentNM();
 
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index a548c959e..3ad45d5be 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -140,7 +140,7 @@ class BvInstantiator : public Instantiator
       Node pv,
       Node n,
       std::vector<Node>& children,
-      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+      std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
   /** process literal, called from processAssertion
    *
    * lit is the literal to solve for pv that has been rewritten according to
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index b351dc83c..c1ad63fc8 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -61,7 +61,7 @@ Node getPvCoeff(TNode pv, TNode n)
 Node normalizePvMult(
     TNode pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   bool neg, neg_coeff = false;
   bool found_pv = false;
@@ -141,7 +141,7 @@ namespace {
 bool isLinearPlus(
     TNode n,
     TNode pv,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   Node coeff;
   Assert(n.getAttribute(BvLinearAttribute()));
@@ -165,7 +165,7 @@ bool isLinearPlus(
 Node normalizePvPlus(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   NodeManager* nm;
   NodeBuilder<> nb_c(BITVECTOR_PLUS);
@@ -254,7 +254,7 @@ Node normalizePvPlus(
 Node normalizePvEqual(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv)
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv)
 {
   Assert(children.size() == 2);
 
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 7c72a29f2..8427f3df8 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -63,7 +63,7 @@ Node getPvCoeff(TNode pv, TNode n);
 Node normalizePvMult(
     TNode pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 /**
  * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks
@@ -83,7 +83,7 @@ Node normalizePvMult(
 Node normalizePvPlus(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 /**
  * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv
@@ -99,7 +99,7 @@ Node normalizePvPlus(
 Node normalizePvEqual(
     Node pv,
     const std::vector<Node>& children,
-    std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
+    std::unordered_map<Node, bool, NodeHashFunction>& contains_pv);
 
 }  // namespace utils
 }  // namespace quantifiers