diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc
index 217d755ca2..92cc64cece 100644
--- a/ortools/sat/cp_model.cc
+++ b/ortools/sat/cp_model.cc
@@ -736,6 +736,20 @@ IntervalVar CpModelBuilder::NewOptionalFixedSizeIntervalVar(
   return IntervalVar(index, this);
 }
 
+void CpModelBuilder::FixVariable(IntVar var, int64_t value) {
+  FillDomainInProto(Domain(value), cp_model_.mutable_variables(var.index()));
+}
+
+void CpModelBuilder::FixVariable(BoolVar var, bool value) {
+  const int index = var.index();
+  if (RefIsPositive(index)) {
+    FillDomainInProto(Domain(value), cp_model_.mutable_variables(index));
+  } else {
+    FillDomainInProto(Domain(!value),
+                      cp_model_.mutable_variables(NegatedRef(index)));
+  }
+}
+
 Constraint CpModelBuilder::AddBoolOr(absl::Span<const BoolVar> literals) {
   ConstraintProto* const proto = cp_model_.add_constraints();
   for (const BoolVar& lit : literals) {
diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h
index 18b29b2c3e..a24ff75d7a 100644
--- a/ortools/sat/cp_model.h
+++ b/ortools/sat/cp_model.h
@@ -23,9 +23,8 @@
  IntVar rabbits = cp_model.NewIntVar(all_animals).WithName("rabbits");
  IntVar pheasants = cp_model.NewIntVar(all_animals).WithName("pheasants");
 
- cp_model.AddEquality(LinearExpr::Sum({rabbits, pheasants}), 20);
- cp_model.AddEquality(LinearExpr::WeightedSum({rabbits, pheasants}, {4, 2}),
- 56);
+ cp_model.AddEquality(rabbits + pheasants, 20);
+ cp_model.AddEquality(4 * rabbits + 2 * pheasants, 56);
 
  const CpSolverResponse response = Solve(cp_model.Build());
  if (response.status() == CpSolverStatus::FEASIBLE) {
@@ -760,6 +759,18 @@ class CpModelBuilder {
   IntervalVar NewOptionalFixedSizeIntervalVar(const LinearExpr& start,
                                               int64_t size, BoolVar presence);
 
+  /// It is sometime convenient when building a model to create a bunch of
+  /// variables that will later be fixed. Instead of doing AddEquality(var,
+  /// value) which add a constraint, these functions modify directly the
+  /// underlying variable domain.
+  ///
+  /// Note that this ignore completely the original variable domain and just fix
+  /// the given variable to the given value, even if it was outside the given
+  /// variable domain. You can still use AddEquality() if this is not what you
+  /// want.
+  void FixVariable(IntVar var, int64_t value);
+  void FixVariable(BoolVar var, bool value);
+
   /// Adds the constraint that at least one of the literals must be true.
   Constraint AddBoolOr(absl::Span<const BoolVar> literals);
 
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 4fbee7c524..cb59049592 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -506,7 +506,7 @@ void FillSolutionInResponse(const CpModelProto& model_proto, const Model& model,
     if (mapping->IsInteger(i)) {
       const IntegerVariable var = mapping->Integer(i);
 
-      // For ignored or not fully instanciated variable, we just use the
+      // For ignored or not fully instantiated variable, we just use the
       // lower bound.
       solution.push_back(model.Get(LowerBound(var)));
     } else {
@@ -2084,6 +2084,9 @@ class FullProblemSolver : public SubSolver {
               *shared_->model_proto, shared_->bounds, local_model_.get());
         }
 
+        // Note that this is done after the loading, so we will never export
+        // problem clauses. We currently also never export binary clauses added
+        // by the initial probing.
         if (shared_->clauses != nullptr) {
           const int id = shared_->clauses->RegisterNewId();
           shared_->clauses->SetWorkerNameForId(id, local_model_->Name());
@@ -2941,26 +2944,27 @@ void SolveCpModelParallel(const CpModelProto& model_proto,
   // Log statistics.
   if (logger->LoggingIsEnabled()) {
     if (parameters.log_subsolver_statistics()) {
-      SOLVER_LOG(logger, "");
-      SOLVER_LOG(logger, "Sub-solver search statistics:");
+      bool first = true;
       for (const auto& subsolver : subsolvers) {
         const std::string stats = subsolver->StatisticsString();
         if (stats.empty()) continue;
+        if (first) {
+          SOLVER_LOG(logger, "");
+          SOLVER_LOG(logger, "Sub-solver search statistics:");
+          first = false;
+        }
         SOLVER_LOG(logger,
                    absl::StrCat("  '", subsolver->name(), "':\n", stats));
       }
     }
 
-    SOLVER_LOG(logger, "");
     shared.response->DisplayImprovementStatistics();
 
     if (shared.bounds) {
-      SOLVER_LOG(logger, "");
       shared.bounds->LogStatistics(logger);
     }
 
     if (shared.clauses) {
-      SOLVER_LOG(logger, "");
       shared.clauses->LogStatistics(logger);
     }
   }
@@ -3557,6 +3561,7 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
           SOLVER_LOG(logger, lp->Statistics());
         }
       }
+      SOLVER_LOG(logger, "");
     }
   }
 
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index b9df049f86..1c2d041da7 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -138,6 +138,9 @@ bool SatSolver::AddClauseDuringSearch(absl::Span<const Literal> literals) {
   if (literals.empty()) return SetModelUnsat();
   if (literals.size() == 1) return AddUnitClause(literals[0]);
   if (literals.size() == 2) {
+    // TODO(user): We generate in some corner cases clauses with
+    // literals[0].Variable() == literals[1].Variable(). Avoid doing that and
+    // adding such binary clauses to the graph?
     if (!binary_implication_graph_->AddBinaryClauseDuringSearch(literals[0],
                                                                 literals[1])) {
       CHECK_EQ(CurrentDecisionLevel(), 0);
@@ -213,7 +216,17 @@ bool SatSolver::AddProblemClauseInternal(absl::Span<const Literal> literals) {
     }
     trail_->EnqueueWithUnitReason(literals[0]);
   } else if (literals.size() == 2) {
-    AddBinaryClauseInternal(literals[0], literals[1]);
+    // TODO(user): Make sure the presolve do not generate such clauses.
+    if (literals[0] == literals[1]) {
+      // Literal must be true.
+      trail_->EnqueueWithUnitReason(literals[0]);
+    } else if (literals[0] == literals[1].Negated()) {
+      // Always true.
+      return true;
+    } else {
+      AddBinaryClauseInternal(literals[0], literals[1],
+                              /*export_clause=*/false);
+    }
   } else {
     if (!clauses_propagator_->AddClause(literals, trail_)) {
       return SetModelUnsat();
@@ -362,6 +375,7 @@ int SatSolver::AddLearnedClauseAndEnqueueUnitPropagation(
 
   if (literals.size() == 2) {
     if (track_binary_clauses_) {
+      // This clause MUST be knew, otherwise something is wrong.
       CHECK(binary_clauses_.Add(BinaryClause(literals[0], literals[1])));
     }
     if (shared_binary_clauses_callback_ != nullptr) {
@@ -438,10 +452,18 @@ void SatSolver::SaveDebugAssignment() {
   }
 }
 
-void SatSolver::AddBinaryClauseInternal(Literal a, Literal b) {
-  if (!track_binary_clauses_ || binary_clauses_.Add(BinaryClause(a, b))) {
-    binary_implication_graph_->AddBinaryClause(a, b);
+void SatSolver::AddBinaryClauseInternal(Literal a, Literal b,
+                                        bool export_clause) {
+  if (track_binary_clauses_) {
+    // Abort if this clause was already added.
+    if (!binary_clauses_.Add(BinaryClause(a, b))) return;
   }
+
+  if (export_clause && shared_binary_clauses_callback_ != nullptr) {
+    shared_binary_clauses_callback_(a, b);
+  }
+
+  binary_implication_graph_->AddBinaryClause(a, b);
 }
 
 bool SatSolver::ClauseIsValidUnderDebugAssignment(
@@ -905,11 +927,7 @@ bool SatSolver::AddBinaryClauses(const std::vector<BinaryClause>& clauses) {
   SCOPED_TIME_STAT(&stats_);
   CHECK_EQ(CurrentDecisionLevel(), 0);
   for (const BinaryClause c : clauses) {
-    if (trail_->Assignment().LiteralIsFalse(c.a) &&
-        trail_->Assignment().LiteralIsFalse(c.b)) {
-      return SetModelUnsat();
-    }
-    AddBinaryClauseInternal(c.a, c.b);
+    if (!AddBinaryClause(c.a, c.b)) return false;
   }
   if (!Propagate()) return SetModelUnsat();
   return true;
@@ -1081,7 +1099,7 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
     counters_.minimization_num_removed_literals += clause->size() - 2;
 
     // The order is important for the drat proof.
-    AddBinaryClauseInternal(candidate[0], candidate[1]);
+    AddBinaryClauseInternal(candidate[0], candidate[1], /*export_clause=*/true);
     clauses_propagator_->Detach(clause);
 
     // This is needed in the corner case where this was the first binary clause
@@ -1581,7 +1599,8 @@ void SatSolver::ProcessNewlyFixedVariables() {
       // This clause is now a binary clause, treat it separately. Note that
       // it is safe to do that because this clause can't be used as a reason
       // since we are at level zero and the clause is not satisfied.
-      AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral());
+      AddBinaryClauseInternal(clause->FirstLiteral(), clause->SecondLiteral(),
+                              /*export_clause=*/true);
       clauses_propagator_->LazyDetach(clause);
       ++num_binary;
       continue;
diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h
index 6cb8fa0d1c..ffe6a633c2 100644
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -452,7 +452,10 @@ class SatSolver {
 
   // Adds a binary clause to the BinaryImplicationGraph and to the
   // BinaryClauseManager when track_binary_clauses_ is true.
-  void AddBinaryClauseInternal(Literal a, Literal b);
+  //
+  // If export_clause is true, then we will also export_clause that to a
+  // potential shared_binary_clauses_callback_.
+  void AddBinaryClauseInternal(Literal a, Literal b, bool export_clause);
 
   // See SaveDebugAssignment(). Note that these functions only consider the
   // variables at the time the debug_assignment_ was saved. If new variables
diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc
index 08fd96ee95..ed81dfdcdd 100644
--- a/ortools/sat/synchronization.cc
+++ b/ortools/sat/synchronization.cc
@@ -688,6 +688,7 @@ void SharedResponseManager::RegisterObjectiveBoundImprovement(
 void SharedResponseManager::DisplayImprovementStatistics() {
   absl::MutexLock mutex_lock(&mutex_);
   if (!primal_improvements_count_.empty()) {
+    SOLVER_LOG(logger_, "");
     SOLVER_LOG(logger_, "Solutions found per subsolver:");
     for (const auto& entry : primal_improvements_count_) {
       SOLVER_LOG(logger_, "  '", entry.first, "': ", entry.second);
@@ -842,6 +843,7 @@ void SharedBoundsManager::GetChangedBounds(
 void SharedBoundsManager::LogStatistics(SolverLogger* logger) {
   absl::MutexLock mutex_lock(&mutex_);
   if (!bounds_exported_.empty()) {
+    SOLVER_LOG(logger, "");
     SOLVER_LOG(logger, "Improving variable bounds shared per subsolver:");
     for (const auto& entry : bounds_exported_) {
       SOLVER_LOG(logger, "  '", entry.first, "': ", entry.second);
@@ -906,6 +908,7 @@ void SharedClausesManager::LogStatistics(SolverLogger* logger) {
     name_to_clauses[id_to_worker_name_[id]] = id_to_clauses_exported_[id];
   }
   if (!name_to_clauses.empty()) {
+    SOLVER_LOG(logger, "");
     SOLVER_LOG(logger, "Clauses shared per subsolver:");
     for (const auto& entry : name_to_clauses) {
       SOLVER_LOG(logger, "  '", entry.first, "': ", entry.second);