From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 12 Nov 2014 17:31:00 +0000 (-0500)
Subject: BV inequality graph TNode fix.
X-Git-Tag: cvc5-1.0.0~6501^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=381e9119136fa76bf4a6369e378c98c4998f705c;p=cvc5.git

BV inequality graph TNode fix.
---

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;