fixing bv inequality solver explanation bug

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index feb061ee1..ff344d307 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -141,6 +141,11 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
         // it means we have an overflow and hence a conflict
         std::vector<TermId> conflict;
         conflict.push_back(it->reason);
+        Assert (hasModelValue(start));
+        ReasonId start_reason = getModelValue(start).reason;
+        if (start_reason != UndefinedReasonId) {
+          conflict.push_back(start_reason);
+        }
         computeExplanation(start, current, conflict);
         Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
         setConflict(conflict); 
@@ -261,6 +266,7 @@ ReasonId InequalityGraph::registerReason(TNode reason) {
   ReasonId id = d_reasonNodes.size();
   d_reasonNodes.push_back(reason);
   d_reasonToIdMap[reason] = id;
+  Debug("bv-inequality-internal") << "InequalityGraph::registerReason " << reason << " => id"<< id << "\n"; 
   return id; 
 }