diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index afd88fcd4c..81c0aa4306 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -158,8 +158,8 @@ std::string ValidateLinearConstraint(const CpModelProto& model,
     // Note that we use min/max with zero to disallow "alternative" terms and
     // be sure that we cannot have an overflow if we do the computation in a
     // different order.
-    sum_min = CapAdd(sum_min, std::min(0ll, std::min(prod1, prod2)));
-    sum_max = CapAdd(sum_max, std::max(0ll, std::max(prod1, prod2)));
+    sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
+    sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
     for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
       if (v == kint64max || v == kint64min) {
         return "Possible integer overflow in constraint: " +
@@ -221,8 +221,8 @@ std::string ValidateObjective(const CpModelProto& model,
     // Note that we use min/max with zero to disallow "alternative" terms and
     // be sure that we cannot have an overflow if we do the computation in a
     // different order.
-    sum_min = CapAdd(sum_min, std::min(0ll, std::min(prod1, prod2)));
-    sum_max = CapAdd(sum_max, std::max(0ll, std::max(prod1, prod2)));
+    sum_min = CapAdd(sum_min, std::min(int64{0}, std::min(prod1, prod2)));
+    sum_max = CapAdd(sum_max, std::max(int64{0}, std::max(prod1, prod2)));
     for (const int64 v : {prod1, prod2, sum_min, sum_max}) {
       // When introducing the objective variable, we use a [...] domain so we
       // need to be more defensive here to make sure no overflow can happen in
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index 817f2d377a..bc4166d0ee 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -477,7 +477,7 @@ bool PresolveIntMax(ConstraintProto* ct, PresolveContext* context) {
     if (gtl::ContainsKey(used_ref, ref)) continue;
     if (gtl::ContainsKey(used_ref, NegatedRef(ref)) ||
         ref == NegatedRef(target_ref)) {
-      target_min = std::max(target_min, 0ll);
+      target_min = std::max(target_min, int64{0});
     }
     used_ref.insert(ref);
     ct->mutable_int_max()->set_vars(new_size++, ref);
@@ -1850,7 +1850,9 @@ void PresolveCpModel(CpModelProto* presolved_model, CpModelProto* mapping_model,
   //
   // TODO(user): expose the parameters here so we can use
   // cp_model_use_sat_presolve().
-  PresolvePureSatPart(&context);
+  if (!context.is_unsat) {
+    PresolvePureSatPart(&context);
+  }
 
   if (context.is_unsat) {
     // Set presolved_model to the simplest UNSAT problem (empty clause).
diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md
index 6a15850e3e..9647fd4b6c 100644
--- a/ortools/sat/doc/boolean_logic.md
+++ b/ortools/sat/doc/boolean_logic.md
@@ -18,7 +18,7 @@ negation of 'x'.
 ### Python code
 
 ```python
-from google3.util.operations_research.sat.python import cp_model
+from ortools.sat.python import cp_model
 
 model = cp_model.CpModel()
 
@@ -30,24 +30,26 @@ not_x = x.Not()
 ### C++ code
 
 ```cpp
-#include "util/operations_research/sat/cp_model.pb.h"
-#include "util/operations_research/sat/cp_model_utils.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_utils.h"
 
 namespace operations_research {
 namespace sat {
 
-CpModelProto cp_model;
+void LiteralSample() {
+  CpModelProto cp_model;
 
-auto new_boolean_variable = [&cp_model]() {
-  const int index = cp_model.variables_size();
-  IntegerVariableProto* const var = cp_model.add_variables();
-  var->add_domain(0);
-  var->add_domain(1);
-  return index;
-};
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
 
-const int x = new_boolean_variable();
-const int not_x = NegatedRef(x);
+  const int x = new_boolean_variable();
+  const int not_x = NegatedRef(x);
+}
 
 }  // namespace sat
 }  // namespace operations_research
@@ -89,7 +91,7 @@ constraints. For instance, we can add a constraint Or(x, not(y)).
 ### Python code
 
 ```python
-from google3.util.operations_research.sat.python import cp_model
+from ortools.sat.python import cp_model
 
 model = cp_model.CpModel()
 
@@ -102,34 +104,35 @@ model.AddBoolOr([x, y.Not()])
 ### C++ code
 
 ```cpp
-#include "util/operations_research/sat/cp_model.pb.h"
-#include "util/operations_research/sat/cp_model_utils.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_utils.h"
 
 namespace operations_research {
 namespace sat {
 
-CpModelProto cp_model;
+void BoolOrSample() {
+  CpModelProto cp_model;
 
-auto new_boolean_variable = [&cp_model]() {
-  const int index = cp_model.variables_size();
-  IntegerVariableProto* const var = cp_model.add_variables();
-  var->add_domain(0);
-  var->add_domain(1);
-  return index;
-};
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
 
-auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
-  BooleanArgumentProto* const bool_or =
-      model.add_constraints()->mutable_bool_or();
-  for (const int lit : literals) {
-    mutable_bool_or->add_literals(lit);
-  }
-};
-
-const int x = new_boolean_variable();
-const int y = new_boolean_variable();
-add_bool_or({x, NegatedRef(y)});
+  auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
+    BooleanArgumentProto* const bool_or =
+        model.add_constraints()->mutable_bool_or();
+    for (const int lit : literals) {
+      mutable_bool_or->add_literals(lit);
+    }
+  };
 
+  const int x = new_boolean_variable();
+  const int y = new_boolean_variable();
+  add_bool_or({x, NegatedRef(y)});
+}
 }  // namespace sat
 }  // namespace operations_research
 ```
@@ -176,7 +179,7 @@ then is written as Or(not b, x) and Or(not b, not y).
 ### Python code
 
 ```python
-from google3.util.operations_research.sat.python import cp_model
+from ortools.sat.python import cp_model
 
 model = cp_model.CpModel()
 
@@ -199,49 +202,51 @@ model.AddBoolOt([b.Not(), y.Not()])
 ### C++ code
 
 ```cpp
-#include "util/operations_research/sat/cp_model.pb.h"
-#include "util/operations_research/sat/cp_model_utils.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_utils.h"
 
 namespace operations_research {
 namespace sat {
 
-CpModelProto cp_model;
+void ReifiedSample() {
+  CpModelProto cp_model;
 
-auto new_boolean_variable = [&cp_model]() {
-  const int index = cp_model.variables_size();
-  IntegerVariableProto* const var = cp_model.add_variables();
-  var->add_domain(0);
-  var->add_domain(1);
-  return index;
-};
+  auto new_boolean_variable = [&cp_model]() {
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(0);
+    var->add_domain(1);
+    return index;
+  };
 
-auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
-  BooleanArgumentProto* const bool_or =
-      model.add_constraints()->mutable_bool_or();
-  for (const int lit : literals) {
-    mutable_bool_or->add_literals(lit);
-  }
-};
+  auto add_bool_or = [&cp_model](const std::vector<int>& literals) {
+    BooleanArgumentProto* const bool_or =
+        model.add_constraints()->mutable_bool_or();
+    for (const int lit : literals) {
+      mutable_bool_or->add_literals(lit);
+    }
+  };
 
-auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
-                                        const int literal) {
-  Constraint* const ct = model.add_constraints();
-  ct->add_enforcement_literal(literal);
-  for (const int lit : literals) {
-    ct->mutable_bool_and()->add_literals(lit);
-  }
-};
+  auto add_reified_bool_and = [&cp_model](const std::vector<int>& literals,
+                                          const int literal) {
+    Constraint* const ct = model.add_constraints();
+    ct->add_enforcement_literal(literal);
+    for (const int lit : literals) {
+      ct->mutable_bool_and()->add_literals(lit);
+    }
+  };
 
-const int x = new_boolean_variable();
-const int y = new_boolean_variable();
-const int b = new_boolean_variable();
+  const int x = new_boolean_variable();
+  const int y = new_boolean_variable();
+  const int b = new_boolean_variable();
 
-// First version using a half-reified bool and.
-add_reified_bool_and({x, NegatedRef(y)}, b);
+  // First version using a half-reified bool and.
+  add_reified_bool_and({x, NegatedRef(y)}, b);
 
-// Second version using implications.
-add_bool_or({NegatedRef(b), x});
-add_bool_or({NegatedRef(b), NegatedRef(y)});
+  // Second version using bool or.
+  add_bool_or({NegatedRef(b), x});
+  add_bool_or({NegatedRef(b), NegatedRef(y)});
+}
 
 }  // namespace sat
 }  // namespace operations_research
@@ -279,4 +284,4 @@ public class CodeSamplesSat
     ReifiedSample();
   }
 }
-```
\ No newline at end of file
+```
diff --git a/ortools/sat/doc/index.md b/ortools/sat/doc/index.md
index e24b4d7b08..eb5dcd361d 100644
--- a/ortools/sat/doc/index.md
+++ b/ortools/sat/doc/index.md
@@ -20,8 +20,8 @@ The Python interface to the CP-SAT solver is implemented using two classes.
 *   The **CpModel** class proposes modeling methods that creates variables, or
     add constraints. This class completely hides the underlying *CpModelProto*
     used to store the model.
-*   The **CpSolver** class encapsulates the solve API. and offers
-    helpers to access the solution found by the solve.
+*   The **CpSolver** class encapsulates the solve API. and offers helpers to
+    access the solution found by the solve.
 
 ```python
 from ortools.sat.python import cp_model
@@ -34,7 +34,8 @@ x = model.NewBoolVar('x')
 ## C++ code samples
 
 The interface to the C++ CP-SAT solver is implemented through the
-**CpModelProto** class described in *ortools/sat/cp_model.proto*.
+**CpModelProto** class described in
+*ortools/sat/cp_model.proto*.
 
 To help creating variables and constraints, we propose some inline helpers to
 improve readability.
@@ -64,7 +65,7 @@ void CodeSample() {
 }  // namespace operations_research
 ```
 
-## C\# code
+## C\# code samples
 
 The C\# code implements the same interface as the python code, with a
 **CpModel**, and a **CpSolver** class.
@@ -75,14 +76,16 @@ using Google.OrTools.Sat;
 
 public class CodeSamplesSat
 {
-  static void CodeSample() {
+  static void CodeSample()
+  {
     // Creates the model.
     CpModel model = new CpModel();
     // Creates the Boolean variable.
     IntVar x = model.NewBoolVar("x");
   }
 
-  static void Main() {
+  static void Main()
+  {
     CodeSample();
   }
 }
diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md
index 9b10c7d875..9628ecdcf9 100644
--- a/ortools/sat/doc/scheduling.md
+++ b/ortools/sat/doc/scheduling.md
@@ -41,35 +41,37 @@ interval_var = model.NewIntervalVar(start_var, duration, end_var, 'interval')
 namespace operations_research {
 namespace sat {
 
-CpModelProto cp_model;
+void IntervalSample() {
+  CpModelProto cp_model;
 
-auto new_variable = [&cp_model](int64 lb, int64 ub) {
-  CHECK_LE(lb, ub);
-  const int index = cp_model.variables_size();
-  IntegerVariableProto* const var = cp_model.add_variables();
-  var->add_domain(lb);
-  var->add_domain(ub);
-  return index;
-};
+  auto new_variable = [&cp_model](int64 lb, int64 ub) {
+    CHECK_LE(lb, ub);
+    const int index = cp_model.variables_size();
+    IntegerVariableProto* const var = cp_model.add_variables();
+    var->add_domain(lb);
+    var->add_domain(ub);
+    return index;
+  };
 
-auto new_constant = [&cp_model, &new_variable](int64 v) {
-  return new_variable(v, v);
-};
+  auto new_constant = [&cp_model, &new_variable](int64 v) {
+    return new_variable(v, v);
+  };
 
-auto new_interval = [&cp_model](int start, int duration, int end) {
-  const int index = cp_model.constraints_size();
-  IntervalConstraintProto* const interval =
-      cp_model.add_constraints()->mutable_interval();
-  interval_proto->set_start(start);
-  interval_proto->set_size(duration);
-  interval_proto->set_end(end);
-  return index;
-};
+  auto new_interval = [&cp_model](int start, int duration, int end) {
+    const int index = cp_model.constraints_size();
+    IntervalConstraintProto* const interval =
+        cp_model.add_constraints()->mutable_interval();
+    interval_proto->set_start(start);
+    interval_proto->set_size(duration);
+    interval_proto->set_end(end);
+    return index;
+  };
 
-const int start_var = new_variable(0, horizon);
-const int duration_var = new_constant(10);
-const int end_var = new_variable(0, horizon);
-const int interval_var = new_interval(start_var, duration_var, end_var);
+  const int start_var = new_variable(0, horizon);
+  const int duration_var = new_constant(10);
+  const int end_var = new_variable(0, horizon);
+  const int interval_var = new_interval(start_var, duration_var, end_var);
+}
 
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md
index 557052b595..68d57cc5b7 100644
--- a/ortools/sat/doc/solver.md
+++ b/ortools/sat/doc/solver.md
@@ -1,12 +1,12 @@
 # Solving a CP-SAT model
 
-https://developers.google.com/optimization/
 
 
 ## Searching for one (optimal) solution
 
-By default, search for one solution will return the first solution found if the
-model has no objective, or the optimal solution if the model has an objective.
+By default, searching for one solution will return the first solution found if
+the model has no objective, or the optimal solution if the model has an
+objective.
 
 ### Python solver code
 
@@ -22,8 +22,7 @@ x = model.NewBoolVar('x')
 # Create a solver and solve.
 solver = cp_model.CpSolver()
 status = solver.Solve(model)
-if status == cp_model.OPTIMAL:
-  print("Objective value: %i" % solver.ObjectiveValue())  # if defined.
+if status == cp_model.MODEL_SAT:
   print('x= %i' %  solver.Value(x))
 ```
 
@@ -73,7 +72,10 @@ void SimpleSolve() {
 } // namespace operations_research
 ```
 
-### C\# solver code
+### C\# code
+
+As in python, the CpSolver class encapsulates searching for a solution of a
+model.
 
 ```cs
 using System;
@@ -115,8 +117,8 @@ public class CodeSamplesSat
 
 ## Changing the parameters of the solver
 
-The SatParameters protobuf encapsulate a set of parameters of a CP-SAT solver.
-The most useful one is the time limit.
+The SatParameters protobuf encapsulates the set of parameters of a CP-SAT
+solver. The most useful one is the time limit.
 
 ### Specifying the time limit in python
 
@@ -182,7 +184,6 @@ void SolveWithTimeLimit() {
   if (response.status() == CpSolverStatus::MODEL_SAT) {
     // Get the value of x in the solution.
     const int64 value_x = response.solution(x);
-    LOG(INFO) << "x = " << value_x;
   }
 }
 
@@ -238,7 +239,7 @@ public class CodeSamplesSat
 
 ## Printing intermediate solutions
 
-In an optimization model, you can print intermediate solution. You need to
+In an optimization model, you can print intermediate solutions. You need to
 register a callback on the solver that will be called at each solution.
 
 The exact implementation depends on the target language.
@@ -277,11 +278,11 @@ def MinimalCpSatPrintIntermediateSolutions():
   x = model.NewIntVar(0, num_vals - 1, "x")
   y = model.NewIntVar(0, num_vals - 1, "y")
   z = model.NewIntVar(0, num_vals - 1, "z")
-  # Create the constraints.
+  # Creates the constraints.
   model.Add(x != y)
   model.Maximize(x + 2 * y + 3 * z)
 
-  # Create a solver and solve.
+  # Creates a solver and solve.
   solver = cp_model.CpSolver()
   solution_printer = VarArraySolutionPrinter([x, y, z])
   status = solver.SolveWithSolutionObserver(model, solution_printer)
@@ -402,7 +403,6 @@ public class VarArraySolutionPrinterWithObjective : CpSolverSolutionCallback
   private IntVar[] variables_;
 }
 
-
 public class CodeSamplesSat
 {
   static void MinimalCpSatPrintIntermediateSolutions()
@@ -417,7 +417,7 @@ public class CodeSamplesSat
     IntVar z = model.NewIntVar(0, num_vals - 1, "z");
     // Creates the constraints.
     model.Add(x != y);
-    // Create the objective.
+    // Creates the objective.
     model.Maximize(x + 2 * y + 3 * z);
 
     // Creates a solver and solves the model.
@@ -445,6 +445,8 @@ The exact implementation depends on the target language.
 
 ### Python code
 
+To search for all solutions, the SearchForAllSolutions method must be used.
+
 ```python
 from ortools.sat.python import cp_model
 
@@ -476,10 +478,10 @@ def MinimalSatSearchForAllSolutions():
   x = model.NewIntVar(0, num_vals - 1, "x")
   y = model.NewIntVar(0, num_vals - 1, "y")
   z = model.NewIntVar(0, num_vals - 1, "z")
-  # Create the constraints.
+  # Creates the constraint.
   model.Add(x != y)
 
-  # Create a solver and solve.
+  # Creates a solver and solve.
   solver = cp_model.CpSolver()
   solution_printer = VarArraySolutionPrinter([x, y, z])
   status = solver.SearchForAllSolutions(model, solution_printer)
@@ -489,6 +491,8 @@ def MinimalSatSearchForAllSolutions():
 
 ### C++ code
 
+To search for all solution, a parameter of the sat solver must be changed.
+
 ```cpp
 #include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_solver.h"
@@ -555,6 +559,8 @@ void MinimalSatSearchForAllSolutions() {
 
 ### C\# code
 
+As in python, CpSolver.SearchAllSolutions() must be called.
+
 ```cs
 using System;
 using Google.OrTools.Sat;
@@ -619,4 +625,4 @@ public class CodeSamplesSat
     MinimalCpSatAllSolutions();
   }
 }
-```
\ No newline at end of file
+```
diff --git a/ortools/sat/drat_checker.cc b/ortools/sat/drat_checker.cc
index 862f9bbfa9..d9bd32cbf9 100644
--- a/ortools/sat/drat_checker.cc
+++ b/ortools/sat/drat_checker.cc
@@ -98,8 +98,8 @@ ClauseIndex DratChecker::AddClause(absl::Span<Literal> clause) {
   for (int i = first_literal_index + 1; i < literals_.size(); ++i) {
     CHECK(literals_[i] != literals_[i - 1].Negated());
   }
-  clauses_.push_back(Clause(first_literal_index,
-                            literals_.size() - first_literal_index));
+  clauses_.emplace_back(first_literal_index,
+                        literals_.size() - first_literal_index);
   if (!clause.empty()) {
     num_variables_ =
         std::max(num_variables_, literals_.back().Variable().value() + 1);
diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc
index dad3333344..390841e5ab 100644
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -271,6 +271,7 @@ bool LinearProgrammingConstraint::Propagate() {
         lp_data_.SetConstraintBounds(row, cut.lb, cut.ub);
         for (int i = 0; i < cut.vars.size(); ++i) {
           const glop::ColIndex col = GetOrCreateMirrorVariable(cut.vars[i]);
+
           // The returned coefficients correspond to variables at the CP scale,
           // so we need to divide them by CpToLpScalingFactor() which is the
           // same as multiplying by LpToCpScalingFactor().