From b8b51a0c359628d7202a8a5ff0c2a4beb4c041e9 Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Thu, 29 Dec 2016 15:43:04 -0800
Subject: [PATCH] Changing a set of TNodes to a set of Nodes in the BV
 inequality solver. The ref count of the TNodes in the set can become 0. Set
 operations containing garbage collected TNodes could then fail.

---
 src/theory/bv/bv_subtheory_inequality.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 5fbdf74ab..617e3b761 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -47,8 +47,8 @@ class InequalitySolver: public SubtheorySolver {
   InequalityGraph d_inequalityGraph;
   context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations;
   context::CDO<bool> d_isComplete;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet;
-  TNodeSet d_ineqTerms;
+  typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
+  NodeSet d_ineqTerms;
   bool isInequalityOnly(TNode node);
   bool addInequality(TNode a, TNode b, bool strict, TNode fact);
   Statistics d_statistics;
-- 
2.30.2