From 703f4c52d6e5eecb1488edade036810214c033f3 Mon Sep 17 00:00:00 2001
From: Laurent Perron <lperron@google.com>
Date: Wed, 29 Sep 2021 16:36:42 +0200
Subject: [PATCH] fix

---
 ortools/sat/integer_expr.cc | 8 ++------
 ortools/sat/integer_expr.h  | 8 ++++----
 2 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/ortools/sat/integer_expr.cc b/ortools/sat/integer_expr.cc
index 4ccf90ea77..13ba7690ba 100644
--- a/ortools/sat/integer_expr.cc
+++ b/ortools/sat/integer_expr.cc
@@ -835,7 +835,6 @@ bool PositiveDivisionPropagator::Propagate() {
   // If min_div == 0 we can't deduce anything.
   // Otherwise, denom <= num / min_div and denom <= max_num / min_div.
   if (min_div > 0) {
-    // const IntegerValue new_max_denom = (max_num - 1) / (min_div - 1);
     const IntegerValue new_max_denom = max_num / min_div;
     if (max_denom > new_max_denom) {
       if (!integer_trail_->Enqueue(
@@ -847,11 +846,8 @@ bool PositiveDivisionPropagator::Propagate() {
     }
   }
 
-  // We start from num / denom <= max_div.
-  // num < (max_div + 1) * denom.
-  // num + 1 <= (max_div + 1) * denom.
-  // denom >= CeilRatio(num + 1, max_div+1) >= CeilRatio(min_num + 1, max_div +
-  // 1).
+  // denom >= CeilRatio(num + 1, max_div+1)
+  //               >= CeilRatio(min_num + 1, max_div +).
   const IntegerValue new_min_denom = CeilRatio(min_num + 1, max_div + 1);
   if (min_denom < new_min_denom) {
     if (!integer_trail_->Enqueue(
diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h
index 32694d6635..d9b8a417ea 100644
--- a/ortools/sat/integer_expr.h
+++ b/ortools/sat/integer_expr.h
@@ -230,9 +230,9 @@ class PositiveProductPropagator : public PropagatorInterface {
   DISALLOW_COPY_AND_ASSIGN(PositiveProductPropagator);
 };
 
-// Propagates a / b = c. Basic version, we don't extract any special cases, and
-// we only propagates the bounds.
-// It expects a, and c to be >= 0, b to be > 0.
+// Propagates num / denom = div. Basic version, we don't extract any special
+// cases, and we only propagates the bounds. It expects num, div to be >= 0,
+// and denom to be > 0.
 //
 // TODO(user): Deal with overflow.
 class PositiveDivisionPropagator : public PropagatorInterface {
@@ -807,7 +807,7 @@ inline std::function<void(Model*)> ProductConstraint(IntegerVariable a,
   };
 }
 
-// Adds the constraint: num / b = c.
+// Adds the constraint: num / denom = div.
 inline std::function<void(Model*)> DivisionConstraint(IntegerVariable num,
                                                       IntegerVariable denom,
                                                       IntegerVariable div) {