diff --git a/ortools/constraint_solver/element.cc b/ortools/constraint_solver/element.cc
index 0ba81daa40..4cc243aeae 100644
--- a/ortools/constraint_solver/element.cc
+++ b/ortools/constraint_solver/element.cc
@@ -338,7 +338,8 @@ class IntExprElement : public BaseIntExprElement {
   }
   int64 ExprMin() const override { return std::max<int64>(0, expr_->Min()); }
   int64 ExprMax() const override {
-    return std::min<int64>(values_.size() - 1, expr_->Max());
+    return values_.empty() ? 0
+                           : std::min<int64>(values_.size() - 1, expr_->Max());
   }
 
  private:
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index fa8a874100..bdb5de4db7 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -2217,14 +2217,6 @@ void ExpandObjective(PresolveContext* context) {
     }
   }
 
-  // Convert the objective linear expression to a map for ease of use below.
-  std::map<int, int64> objective_map;
-  for (int i = 0; i < context->working_model->objective().vars_size(); ++i) {
-    const int ref = context->working_model->objective().vars(i);
-    const int64 coeff = context->working_model->objective().coeffs(i);
-    objective_map[PositiveRef(ref)] = RefIsPositive(ref) ? coeff : -coeff;
-  }
-
   // To avoid a bad complexity, we need to compute the number of relevant
   // constraints for each variables.
   const int num_variables = context->working_model->variables_size();
@@ -2248,22 +2240,39 @@ void ExpandObjective(PresolveContext* context) {
     }
   }
 
+  // Convert the objective linear expression to a map for ease of use below.
+  std::map<int, int64> objective_map;
+  std::set<int> var_to_process;
+  for (int i = 0; i < context->working_model->objective().vars_size(); ++i) {
+    const int ref = context->working_model->objective().vars(i);
+    const int64 coeff = context->working_model->objective().coeffs(i);
+    objective_map[PositiveRef(ref)] = RefIsPositive(ref) ? coeff : -coeff;
+    if (var_to_num_relevant_constraints[PositiveRef(ref)] != 0) {
+      var_to_process.insert(PositiveRef(ref));
+    }
+  }
+
   // We currently never expand a variable more than once.
   int num_expansions = 0;
   absl::flat_hash_set<int> processed_vars;
   while (!relevant_constraints.empty()) {
     // Find a not yet expanded var.
     int objective_var = -1;
-    for (const auto& entry : objective_map) {
-      const int var = entry.first;
-      if (processed_vars.count(var)) continue;
-      if (var_to_num_relevant_constraints[var] == 0) continue;
+    while (!var_to_process.empty()) {
+      const int var = *var_to_process.begin();
+      CHECK(!processed_vars.count(var));
+      if (var_to_num_relevant_constraints[var] == 0) {
+        processed_vars.insert(var);
+        var_to_process.erase(var);
+        continue;
+      }
       objective_var = var;
       break;
     }
     if (objective_var == -1) break;
     CHECK(RefIsPositive(objective_var));
     processed_vars.insert(objective_var);
+    var_to_process.erase(objective_var);
 
     int expanded_linear_index = -1;
     int64 objective_coeff_in_expanded_constraint;
@@ -2342,10 +2351,14 @@ void ExpandObjective(PresolveContext* context) {
         if (!RefIsPositive(ref)) coeff = -coeff;
         if (!gtl::ContainsKey(objective_map, var)) {
           context->var_to_constraints[var].insert(-1);
+          if (!gtl::ContainsKey(processed_vars, var)) {
+            var_to_process.insert(var);
+          }
         }
         objective_map[var] += coeff;
         if (objective_map[var] == 0.0) {
           objective_map.erase(var);
+          var_to_process.erase(var);
           context->var_to_constraints[var].erase(-1);
         }
       }
@@ -2735,7 +2748,7 @@ void RemoveUnusedEquivalentVariables(PresolveContext* context) {
 // - All the variables domain will be copied to the mapping_model.
 // - Everything will be remapped so that only the variables appearing in some
 //   constraints will be kept and their index will be in [0, num_new_variables).
-void PresolveCpModel(const PresolveOptions& options,
+bool PresolveCpModel(const PresolveOptions& options,
                      CpModelProto* presolved_model, CpModelProto* mapping_model,
                      std::vector<int>* postsolve_mapping) {
   PresolveContext context;
@@ -2819,7 +2832,7 @@ void PresolveCpModel(const PresolveOptions& options,
     // Set presolved_model to the simplest UNSAT problem (empty clause).
     presolved_model->Clear();
     presolved_model->add_constraints()->mutable_bool_or();
-    return;
+    return true;
   }
 
   // Regroup no-overlaps into max-cliques.
@@ -2948,8 +2961,14 @@ void PresolveCpModel(const PresolveOptions& options,
       }
     }
   }
-  CHECK_EQ("", ValidateCpModel(*presolved_model));
-  CHECK_EQ("", ValidateCpModel(*mapping_model));
+
+  // One possible error that is difficult to avoid here: because of our
+  // objective expansion, we might detect a possible overflow...
+  //
+  // TODO(user): We could abort the expansion when this happen.
+  if (!ValidateCpModel(*presolved_model).empty()) return false;
+  if (!ValidateCpModel(*mapping_model).empty()) return false;
+  return true;
 }
 
 void ApplyVariableMapping(const std::vector<int>& mapping,
diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h
index 54c9c3fb1a..de2bef155b 100644
--- a/ortools/sat/cp_model_presolve.h
+++ b/ortools/sat/cp_model_presolve.h
@@ -50,7 +50,12 @@ struct PresolveOptions {
 // TODO(user): Identify disconnected components and returns a vector of
 // presolved model? If we go this route, it may be nicer to store the indices
 // inside the model. We can add a IntegerVariableProto::initial_index;
-void PresolveCpModel(const PresolveOptions& options,
+//
+// Returns false if a non-recoverable error was encountered.
+//
+// TODO(user): Make sure this can never run into this case provided that the
+// initial model is valid!
+bool PresolveCpModel(const PresolveOptions& options,
                      CpModelProto* presolved_model, CpModelProto* mapping_model,
                      std::vector<int>* postsolve_mapping);
 
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 86971b70b6..ba5a39c886 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -47,6 +47,7 @@
 #include "ortools/port/proto_utils.h"
 #include "ortools/sat/circuit.h"
 #include "ortools/sat/clause.h"
+#include "ortools/sat/cp_model.pb.h"
 #include "ortools/sat/cp_model_checker.h"
 #include "ortools/sat/cp_model_expand.h"
 #include "ortools/sat/cp_model_lns.h"
@@ -1150,13 +1151,13 @@ void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
   model->GetOrCreate<SynchronizationFunction>()->f = std::move(f);
 }
 
-void SetObjectiveSynchronizationFunctions(std::function<double()> f,
-                                          std::function<double()> g,
-                                          Model* model) {
+void SetObjectiveSynchronizationFunctions(
+    std::function<double()> objective_best_solution,
+    std::function<double()> objective_best_bound, Model* model) {
   ObjectiveSynchronizationHelper* helper =
       model->GetOrCreate<ObjectiveSynchronizationHelper>();
-  helper->get_external_bound = std::move(f);
-  helper->get_external_best_bound = std::move(g);
+  helper->get_external_best_objective = std::move(objective_best_solution);
+  helper->get_external_best_bound = std::move(objective_best_bound);
 }
 
 #if !defined(__PORTABLE_PLATFORM__)
@@ -1185,6 +1186,63 @@ std::function<SatParameters(Model*)> NewSatParameters(
 }
 
 namespace {
+void LogNewParallelSolution(const std::string& event_or_solution_count,
+                            double time_in_seconds, double obj_lb,
+                            double obj_ub, const std::string& solution_info) {
+  VLOG(1) << absl::StrFormat("#%-5s %6.2fs  obj:[%0.0f,%0.0f]  %s",
+                             event_or_solution_count, time_in_seconds, obj_lb,
+                             obj_ub, solution_info);
+}
+
+void RegisterObjectiveLowerBoundWatcher(
+    const CpModelProto* model_proto,
+    const std::function<void(const CpSolverResponse&)>&
+        external_solution_observer,
+    IntegerVariable objective_var, Model* model) {
+  const auto broadcast_lower_bound =
+      [model_proto, external_solution_observer, objective_var,
+       model](const std::vector<IntegerVariable>& modified_vars) {
+        CpSolverResponse lb_response;
+        lb_response.set_status(CpSolverStatus::UNKNOWN);
+        auto* integer_trail = model->Get<IntegerTrail>();
+        const ObjectiveSynchronizationHelper* const helper =
+            model->GetOrCreate<ObjectiveSynchronizationHelper>();
+        const WorkerInfo* const worker_info = model->GetOrCreate<WorkerInfo>();
+        const CpObjectiveProto& obj = model_proto->objective();
+        const double new_best_bound = ScaleObjectiveValue(
+            obj, integer_trail->LevelZeroLowerBound(objective_var).value());
+        const double current_best_bound = helper->get_external_best_bound();
+        const double current_objective_value =
+            helper->get_external_best_objective();
+
+        // TODO(user): Unit test this lambda.
+        if ((helper->scaling_factor >= 0 &&  // Unset -> = 0.0 -> minimize.
+             new_best_bound > current_best_bound) ||
+            (helper->scaling_factor < 0 &&
+             new_best_bound < current_best_bound)) {
+          DCHECK_EQ(0, lb_response.solution_size());
+          DCHECK_EQ(0, lb_response.solution_lower_bounds_size());
+          DCHECK_EQ(0, lb_response.solution_upper_bounds_size());
+          DCHECK_EQ(lb_response.status(), CpSolverStatus::UNKNOWN);
+          lb_response.set_objective_value(current_objective_value);
+          lb_response.set_best_objective_bound(new_best_bound);
+
+          if (current_objective_value >= new_best_bound) {
+            LogNewParallelSolution("ObjLb", worker_info->global_timer->Get(),
+                                   new_best_bound, current_objective_value,
+                                   worker_info->worker_name);
+          } else {
+            LogNewParallelSolution("ObjUb", worker_info->global_timer->Get(),
+                                   current_objective_value, new_best_bound,
+                                   worker_info->worker_name);
+          }
+          external_solution_observer(lb_response);
+        }
+      };
+
+  model->GetOrCreate<GenericLiteralWatcher>()
+      ->RegisterLevelZeroModifiedVariablesCallback(broadcast_lower_bound);
+}
 
 // Because we also use this function for postsolve, we call it with
 // is_real_solve set to true and avoid doing non-useful work in this case.
@@ -1414,55 +1472,9 @@ CpSolverResponse SolveCpModelInternal(
     external_solution_observer(response);
   };
 
-  CpSolverResponse lb_response;
-  response.set_status(CpSolverStatus::UNKNOWN);
-
   if (watch_objective_lower_bound) {
-    const ObjectiveSynchronizationHelper* const helper =
-        model->GetOrCreate<ObjectiveSynchronizationHelper>();
-    const WorkerInfo* const worker_info = model->GetOrCreate<WorkerInfo>();
-    CHECK(helper != nullptr);
-    CHECK(worker_info != nullptr);
-
-    const auto broadcast_lower_bound =
-        [&model_proto, external_solution_observer, &lb_response, objective_var,
-         helper, worker_info, &wall_timer,
-         model](const std::vector<IntegerVariable>& modified_vars) {
-          auto* integer_trail = model->Get<IntegerTrail>();
-          const CpObjectiveProto& obj = model_proto.objective();
-          const double new_best_bound = ScaleObjectiveValue(
-              obj, integer_trail->LevelZeroLowerBound(objective_var).value());
-          const double current_best_bound = helper->get_external_best_bound();
-          const double current_objective_value = helper->get_external_bound();
-
-          if ((helper->scaling_factor >= 0 &&  // Unset -> = 0.0 -> minimize.
-               new_best_bound > current_best_bound) ||
-              (helper->scaling_factor < 0 &&
-               new_best_bound < current_best_bound)) {
-            DCHECK_EQ(0, lb_response.solution_size());
-            DCHECK_EQ(0, lb_response.solution_lower_bounds_size());
-            DCHECK_EQ(0, lb_response.solution_upper_bounds_size());
-            DCHECK_EQ(lb_response.status(), CpSolverStatus::UNKNOWN);
-            lb_response.set_objective_value(current_objective_value);
-            lb_response.set_best_objective_bound(new_best_bound);
-
-            if (current_objective_value >= new_best_bound) {
-              VLOG(1) << absl::StrFormat("#LB    %6.2fs  obj:[%0.0f,%0.0f]  %s",
-                                         wall_timer.Get(), new_best_bound,
-                                         current_objective_value,
-                                         worker_info->worker_name);
-            } else {
-              VLOG(1) << absl::StrFormat(
-                  "#UB    %6.2fs  obj:[%0.0f,%0.0f]  %s",
-                  worker_info->global_timer->Get(), current_objective_value,
-                  new_best_bound, worker_info->worker_name);
-            }
-            external_solution_observer(lb_response);
-          }
-        };
-
-    model->GetOrCreate<GenericLiteralWatcher>()
-        ->RegisterLevelZeroModifiedVariablesCallback(broadcast_lower_bound);
+    RegisterObjectiveLowerBoundWatcher(&model_proto, external_solution_observer,
+                                       objective_var, model);
   }
 
   // Load solution hint.
@@ -1630,8 +1642,8 @@ void PostsolveResponse(const CpModelProto& model_proto,
     postsolve_model.Add(operations_research::sat::NewSatParameters(params));
   }
   const CpSolverResponse postsolve_response = SolveCpModelInternal(
-      mapping_proto, false, [](const CpSolverResponse&) {}, false,
-      &postsolve_model);
+      mapping_proto, false, [](const CpSolverResponse&) {},
+      /*watch_objective_lower_bound=*/false, &postsolve_model);
   CHECK_EQ(postsolve_response.status(), CpSolverStatus::FEASIBLE);
 
   // We only copy the solution from the postsolve_response to the response.
@@ -1833,8 +1845,9 @@ CpSolverResponse SolveCpModelWithLNS(
   if (synchro != nullptr && synchro->f != nullptr) {
     response = synchro->f();
   } else {
-    response = SolveCpModelInternal(model_proto, /*is_real_solve=*/true,
-                                    observer, false, model);
+    response =
+        SolveCpModelInternal(model_proto, /*is_real_solve=*/true, observer,
+                             /*watch_objective_lower_bound=*/false, model);
   }
   if (response.status() != CpSolverStatus::FEASIBLE) {
     return response;
@@ -1922,7 +1935,7 @@ CpSolverResponse SolveCpModelWithLNS(
                           &postsolve_mapping);
           local_response = SolveCpModelInternal(
               local_problem, true, [](const CpSolverResponse& response) {},
-              false, &local_model);
+              /*watch_objective_lower_bound=*/false, &local_model);
           PostsolveResponse(model_proto, mapping_proto, postsolve_mapping,
                             &local_response);
         }
@@ -2046,8 +2059,8 @@ CpSolverResponse SolveCpModelParallel(
           local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
               stopped);
           const CpSolverResponse local_response = SolveCpModelInternal(
-              model_proto, true, [](const CpSolverResponse& response) {}, false,
-              &local_model);
+              model_proto, true, [](const CpSolverResponse& response) {},
+              /*watch_objective_lower_bound=*/false, &local_model);
 
           absl::MutexLock lock(&mutex);
           if (best_response.status() == CpSolverStatus::UNKNOWN) {
@@ -2097,7 +2110,7 @@ CpSolverResponse SolveCpModelParallel(
         // solution found so far.
         if (MergeOptimizationSolution(r, maximize, &best_response)) {
           // Checks that r is not a pure best-bound improving solution.
-          CHECK(r.status() == CpSolverStatus::FEASIBLE);
+          CHECK_EQ(r.status(), CpSolverStatus::FEASIBLE);
 
           best_response.set_solution_info(
               absl::StrCat(worker_name, " ", r.solution_info()));
@@ -2122,10 +2135,9 @@ CpSolverResponse SolveCpModelParallel(
         local_model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(
             stopped);
 
-        // Stores the name of the worker in the model.
+        // Stores info that will be used for logs in the local model.
         WorkerInfo* worker_info = local_model.GetOrCreate<WorkerInfo>();
         worker_info->worker_name = worker_name;
-        // Stores the global timer used in logs.
         worker_info->global_timer = global_timer;
 
         SetSynchronizationFunction(std::move(solution_synchronization),
@@ -2144,7 +2156,8 @@ CpSolverResponse SolveCpModelParallel(
               worker_id + random_seed, &local_model);
         } else {
           thread_response = SolveCpModelInternal(
-              model_proto, true, solution_observer, true, &local_model);
+              model_proto, true, solution_observer,
+              /*watch_objective_lower_bound=*/true, &local_model);
         }
 
         // Process final solution. Decide which worker has the 'best'
@@ -2253,7 +2266,14 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
     options.log_info = VLOG_IS_ON(1);
     options.parameters = *model->GetOrCreate<SatParameters>();
     options.time_limit = model->GetOrCreate<TimeLimit>();
-    PresolveCpModel(options, &new_model, &mapping_proto, &postsolve_mapping);
+    const bool ok = PresolveCpModel(options, &new_model, &mapping_proto,
+                                    &postsolve_mapping);
+    if (!ok) {
+      LOG(ERROR) << "Error while presolving, likely due to integer overflow.";
+      CpSolverResponse response;
+      response.set_status(CpSolverStatus::MODEL_INVALID);
+      return response;
+    }
     VLOG(1) << CpModelStats(new_model);
     postprocess_solution = [&model_proto, mapping_proto,
                             postsolve_mapping](CpSolverResponse* response) {
@@ -2284,13 +2304,12 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
       [&model_proto, &observers, &num_solutions, &timer,
        &postprocess_solution](const CpSolverResponse& response) {
         const bool maximize = model_proto.objective().scaling_factor() < 0.0;
-        VLOG(1) << absl::StrFormat("#%-5i %6.2fs  obj:[%0.0f,%0.0f]  %s",
-                                   ++num_solutions, timer.Get(),
-                                   maximize ? response.objective_value()
-                                            : response.best_objective_bound(),
-                                   maximize ? response.best_objective_bound()
-                                            : response.objective_value(),
-                                   response.solution_info());
+        LogNewParallelSolution(absl::StrCat(++num_solutions), timer.Get(),
+                               maximize ? response.objective_value()
+                                        : response.best_objective_bound(),
+                               maximize ? response.best_objective_bound()
+                                        : response.objective_value(),
+                               response.solution_info());
 
         if (observers.empty()) return;
         CpSolverResponse copy = response;
@@ -2325,8 +2344,9 @@ CpSolverResponse SolveCpModel(const CpModelProto& model_proto, Model* model) {
     response = SolveCpModelWithLNS(new_model, observer_function, 1, random_seed,
                                    model);
   } else {
-    response = SolveCpModelInternal(new_model, /*is_real_solve=*/true,
-                                    observer_function, false, model);
+    response = SolveCpModelInternal(
+        new_model, /*is_real_solve=*/true, observer_function,
+        /*watch_objective_lower_bound=*/false, model);
   }
 
   postprocess_solution(&response);
diff --git a/ortools/sat/cp_model_solver.h b/ortools/sat/cp_model_solver.h
index a5f9bceabd..0524d2d270 100644
--- a/ortools/sat/cp_model_solver.h
+++ b/ortools/sat/cp_model_solver.h
@@ -63,11 +63,9 @@ void SetSynchronizationFunction(std::function<CpSolverResponse()> f,
                                 Model* model);
 
 // Sets two funtions to query the state of the shared objective.
-//   - f will wait and return the best objective value.
-//   - g will wait and return the best objective 'best bound'.
-void SetObjectiveSynchronizationFunctions(std::function<double()> f,
-                                          std::function<double()> g,
-                                          Model* model);
+void SetObjectiveSynchronizationFunctions(
+    std::function<double()> objective_best_solution,
+    std::function<double()> objective_best_bound, Model* model);
 
 // Allows to change the default parameters with
 //   model->Add(NewSatParameters(parameters_as_string_or_proto))
diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc
index 7552347c6d..771aeefa0f 100644
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -1267,6 +1267,7 @@ void IntegerTrail::AppendNewBounds(std::vector<IntegerLiteral>* output) const {
 
 GenericLiteralWatcher::GenericLiteralWatcher(Model* model)
     : SatPropagator("GenericLiteralWatcher"),
+      time_limit_(model->GetOrCreate<TimeLimit>()),
       integer_trail_(model->GetOrCreate<IntegerTrail>()),
       rev_int_repository_(model->GetOrCreate<RevIntRepository>()) {
   // TODO(user): This propagator currently needs to be last because it is the
@@ -1325,7 +1326,19 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
 
   // Note that the priority may be set to -1 inside the loop in order to restart
   // at zero.
+  int test_limit = 0;
   for (int priority = 0; priority < queue_by_priority_.size(); ++priority) {
+    // We test the time limit from time to time. This is in order to return in
+    // case of slow propagation.
+    //
+    // TODO(user): The queue will not be emptied, but I am not sure the solver
+    // will be left in an usable state. Fix if it become needed to resume
+    // the solve from the last time it was interupted.
+    if (test_limit > 100) {
+      test_limit = 0;
+      if (time_limit_->LimitReached()) break;
+    }
+
     std::deque<int>& queue = queue_by_priority_[priority];
     while (!queue.empty()) {
       const int id = queue.front();
@@ -1383,29 +1396,25 @@ bool GenericLiteralWatcher::Propagate(Trail* trail) {
         UpdateCallingNeeds(trail);
       }
 
-      // If the propagator pushed an integer bound, we revert to priority = 0.
-      if (integer_trail_->num_enqueues() > old_integer_timestamp) {
-        priority = -1;  // Because of the ++priority in the for loop.
-      }
-
-      // If the propagator pushed a literal, we have two options.
+      // If the propagator pushed a literal, we exit in order to rerun all SAT
+      // only propagators first. Note that since a literal was pushed we are
+      // guaranteed to be called again, and we will resume from priority 0.
       if (trail->Index() > old_boolean_timestamp) {
         // Important: for now we need to re-run the clauses propagator each time
         // we push a new literal because some propagator like the arc consistent
         // all diff relies on this.
         //
-        // However, on some problem, it seems to work better to not do that. One
-        // possible reason is that the reason of a "natural" propagation might
-        // be better than one we learned.
-        const bool run_sat_propagators_at_higher_priority = true;
-        if (run_sat_propagators_at_higher_priority) {
-          // We exit in order to rerun all SAT only propagators first. Note that
-          // since a literal was pushed we are guaranteed to be called again,
-          // and we will resume from priority 0.
-          return true;
-        } else {
-          priority = -1;
-        }
+        // TODO(user): However, on some problem, it seems to work better to not
+        // do that. One possible reason is that the reason of a "natural"
+        // propagation might be better than one we learned.
+        return true;
+      }
+
+      // If the propagator pushed an integer bound, we revert to priority = 0.
+      if (integer_trail_->num_enqueues() > old_integer_timestamp) {
+        ++test_limit;
+        priority = -1;  // Because of the ++priority in the for loop.
+        break;
       }
     }
   }
diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h
index c6fc96bf29..a34dd6aa19 100644
--- a/ortools/sat/integer.h
+++ b/ortools/sat/integer.h
@@ -922,6 +922,7 @@ class GenericLiteralWatcher : public SatPropagator {
   // called.
   void UpdateCallingNeeds(Trail* trail);
 
+  TimeLimit* time_limit_;
   IntegerTrail* integer_trail_;
   RevIntRepository* rev_int_repository_;
 
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index 33249fdc8d..2b3a32edff 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -391,7 +391,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
       model->Get<ObjectiveSynchronizationHelper>();
   const bool synchronize_objective =
       solver->AssumptionLevel() == 0 && helper != nullptr &&
-      helper->get_external_bound != nullptr &&
+      helper->get_external_best_objective != nullptr &&
       helper->objective_var != kNoIntegerVariable;
 
   // Note that it is important to do the level-zero propagation if it wasn't
@@ -418,7 +418,7 @@ SatSolver::Status SolveProblemWithPortfolioSearch(
     // Check external objective, and restart if a better one is supplied.
     // TODO(user): Maybe do not check this at each decision.
     if (synchronize_objective) {
-      const double external_bound = helper->get_external_bound();
+      const double external_bound = helper->get_external_best_objective();
       CHECK(helper->get_external_best_bound != nullptr);
       const double external_best_bound = helper->get_external_best_bound();
       IntegerTrail* const integer_trail = model->GetOrCreate<IntegerTrail>();
diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h
index 7f78c325d7..6b02828098 100644
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -113,7 +113,7 @@ struct ObjectiveSynchronizationHelper {
   double scaling_factor = 1.0;
   double offset = 0.0;
   IntegerVariable objective_var = kNoIntegerVariable;
-  std::function<double()> get_external_bound = nullptr;
+  std::function<double()> get_external_best_objective = nullptr;
   std::function<double()> get_external_best_bound = nullptr;
 
   int64 UnscaledObjective(double value) const {
diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc
index d08428f815..eb9902e9a5 100644
--- a/ortools/sat/linear_programming_constraint.cc
+++ b/ortools/sat/linear_programming_constraint.cc
@@ -48,7 +48,9 @@ LinearProgrammingConstraint::LinearProgrammingConstraint(Model* model)
       trail_(model->GetOrCreate<Trail>()),
       model_heuristics_(model->GetOrCreate<SearchHeuristicsVector>()),
       integer_encoder_(model->GetOrCreate<IntegerEncoder>()),
-      dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()) {
+      dispatcher_(model->GetOrCreate<LinearProgrammingDispatcher>()),
+      expanded_lp_solution_(
+          *model->GetOrCreate<LinearProgrammingConstraintLpSolution>()) {
   // Tweak the default parameters to make the solve incremental.
   glop::GlopParameters parameters;
   parameters.set_use_dual_simplex(true);
diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h
index fa20e4b3f8..487453cf6c 100644
--- a/ortools/sat/linear_programming_constraint.h
+++ b/ortools/sat/linear_programming_constraint.h
@@ -34,6 +34,19 @@
 namespace operations_research {
 namespace sat {
 
+// Stores for each IntegerVariable its temporary LP solution.
+//
+// This is shared between all LinearProgrammingConstraint because in the corner
+// case where we have many different LinearProgrammingConstraint and a lot of
+// variable, we could theoretically use up a quadratic amount of memory
+// otherwise.
+//
+// TODO(user): find a better way?
+struct LinearProgrammingConstraintLpSolution
+    : public gtl::ITIVector<IntegerVariable, double> {
+  LinearProgrammingConstraintLpSolution() {}
+};
+
 // A SAT constraint that enforces a set of linear inequality constraints on
 // integer variables using an LP solver.
 //
@@ -287,7 +300,7 @@ class LinearProgrammingConstraint : public PropagatorInterface,
   std::vector<double> level_zero_lp_solution_;
 
   // Same as lp_solution_ but this vector is indexed differently.
-  gtl::ITIVector<IntegerVariable, double> expanded_lp_solution_;
+  LinearProgrammingConstraintLpSolution& expanded_lp_solution_;
 
   // Linear constraints cannot be created or modified after this is registered.
   bool lp_constraint_is_registered_ = false;
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index b597131b85..c1d4faae00 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -2153,7 +2153,8 @@ void SatSolver::MinimizeConflictRecursively(std::vector<Literal>* conflict) {
   int index = 1;
   for (int i = 1; i < conflict->size(); ++i) {
     const BooleanVariable var = (*conflict)[i].Variable();
-    if (trail_->Info(var).trail_index <=
+    if (time_limit_->LimitReached() ||
+        trail_->Info(var).trail_index <=
             min_trail_index_per_level_[DecisionLevel(var)] ||
         !CanBeInferedFromConflictVariables(var)) {
       // Mark the conflict variable as independent. Note that is_marked_[var]