3 files changed, 19 insertions, 3 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; 
 }
 
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 222ba3039..c6a92a439 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -79,7 +79,9 @@ bool InequalitySolver::check(Theory::Effort e) {
   if (!ok) {
     std::vector<TNode> conflict;
     d_inequalityGraph.getConflict(conflict);
-    d_bv->setConflict(utils::flattenAnd(conflict));
+    Node confl = utils::flattenAnd(conflict);
+    d_bv->setConflict(confl);
+    Debug("bv-subtheory-inequality") << "InequalitySolver::conflict:  "<< confl <<"\n";
     return false;
   }
 
@@ -92,6 +94,7 @@ bool InequalitySolver::check(Theory::Effort e) {
       d_bv->lemma(lemmas[i]);
     }
   }
+  Debug("bv-subtheory-inequality") << "InequalitySolver done. ";
   return true;
 }
 
diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 72131d6e7..aef1437a0 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -86,7 +86,8 @@ bool BvToBoolPreprocessor::isConvertibleBvTerm(TNode node) {
       kind == kind::BITVECTOR_AND ||
       kind == kind::BITVECTOR_OR ||
       kind == kind::BITVECTOR_NOT ||
-      kind == kind::BITVECTOR_XOR) {
+      kind == kind::BITVECTOR_XOR ||
+      kind == kind::BITVECTOR_COMP) {
     return true; 
   }
 
@@ -156,7 +157,13 @@ Node BvToBoolPreprocessor::convertBvTerm(TNode node) {
     Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
     return result; 
   }
-  
+
+  if (kind == kind::BITVECTOR_COMP) {
+    Node result = utils::mkNode(kind::EQUAL, node[0], node[1]);
+    addToBoolCache(node, result);
+    Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvTerm " << node <<" => " << result << "\n"; 
+    return result; 
+  }
 
   switch(kind) {
   case kind::BITVECTOR_OR: