From 822cf47dbb9dc703b70aa9d384230c56e7afc285 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Thu, 28 Aug 2014 17:05:49 -0400
Subject: fixing bug580 caused by bad bv inequality explanation

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

(limited to 'src')

diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index aa605de04..f29b8d467 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -146,7 +146,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) {
         if (start_reason != UndefinedReasonId) {
           conflict.push_back(start_reason);
         }
-        computeExplanation(start, current, conflict);
+        computeExplanation(UndefinedTermId, current, conflict);
         Debug("bv-inequality") << "InequalityGraph::addInequality conflict: cycle \n"; 
         setConflict(conflict); 
         return false; 
-- 
cgit v1.2.3