From 779d5912c52fa80e421292ba2f08764b3fbe3551 Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Mon, 26 Sep 2022 15:37:33 +0200
Subject: [PATCH] [CP-SAT] fix bug in lb_tree_search

---
 ortools/sat/integer_expr.cc   | 10 ++++++++++
 ortools/sat/lb_tree_search.cc |  2 ++
 2 files changed, 12 insertions(+)

diff --git a/ortools/sat/integer_expr.cc b/ortools/sat/integer_expr.cc
index 6b63376e0d..f5ece7a23b 100644
--- a/ortools/sat/integer_expr.cc
+++ b/ortools/sat/integer_expr.cc
@@ -90,6 +90,16 @@ void IntegerSumLE::FillIntegerReason() {
 
 std::pair<IntegerValue, IntegerValue> IntegerSumLE::ConditionalLb(
     IntegerLiteral integer_literal, IntegerVariable target_var) const {
+  // The code below is wrong if integer_literal and target_var are the same.
+  // In this case we return the trival bounds.
+  if (PositiveVariable(integer_literal.var) == PositiveVariable(target_var)) {
+    if (integer_literal.var == target_var) {
+      return {kMinIntegerValue, integer_literal.bound};
+    } else {
+      return {integer_literal.Negated().bound, kMinIntegerValue};
+    }
+  }
+
   // Recall that all our coefficient are positive.
   bool literal_var_present = false;
   bool literal_var_present_positively = false;
diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc
index 70f9431630..c5ed2f5383 100644
--- a/ortools/sat/lb_tree_search.cc
+++ b/ortools/sat/lb_tree_search.cc
@@ -535,6 +535,8 @@ SatSolver::Status LbTreeSearch::Search(
     // dive until we beat the best shared bound. Maybe we shouldn't do that.
     const int base_level = sat_solver_->CurrentDecisionLevel();
     while (true) {
+      // TODO(user): We sometimes branch on the objective variable, this should
+      // probably be avoided.
       const LiteralIndex decision =
           search_helper_->GetDecision(search_heuristic_);