summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_inequality_graph.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.cpp')
-rw-r--r--src/theory/bv/bv_inequality_graph.cpp2
1 files changed, 1 insertions, 1 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback