From 381e9119136fa76bf4a6369e378c98c4998f705c Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 12 Nov 2014 12:31:00 -0500
Subject: [PATCH] BV inequality graph TNode fix.

---
 src/theory/bv/bv_inequality_graph.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index f29b8d467..dca679194 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -263,6 +263,7 @@ ReasonId InequalityGraph::registerReason(TNode reason) {
   if (d_reasonToIdMap.find(reason) != d_reasonToIdMap.end()) {
     return d_reasonToIdMap[reason]; 
   }
+  d_reasonSet.insert(reason);
   ReasonId id = d_reasonNodes.size();
   d_reasonNodes.push_back(reason);
   d_reasonToIdMap[reason] = id;
-- 
2.30.2