diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h
index c74f9eb3b1..e92e1dc97f 100644
--- a/ortools/sat/clause.h
+++ b/ortools/sat/clause.h
@@ -479,7 +479,9 @@ class BinaryImplicationGraph : public SatPropagator {
   void Resize(int num_variables);
 
   // Returns true if there is no constraints in this class.
-  bool IsEmpty() { return num_implications_ == 0 && at_most_ones_.empty(); }
+  bool IsEmpty() const final {
+    return num_implications_ == 0 && at_most_ones_.empty();
+  }
 
   // Adds the binary clause (a OR b), which is the same as (not a => b).
   // Note that it is also equivalent to (not b => a).
diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc
index f93c121439..72d3f74bb1 100644
--- a/ortools/sat/cp_model_presolve.cc
+++ b/ortools/sat/cp_model_presolve.cc
@@ -79,9 +79,9 @@ void CpModelPresolver::RemoveEmptyConstraints() {
       context_->working_model->constraints_size();
   for (int c = 0; c < old_num_non_empty_constraints; ++c) {
     const auto type = context_->working_model->constraints(c).constraint_case();
-    if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) continue;
-    if (type == ConstraintProto::ConstraintCase::kDummyConstraint) continue;
-    if (type == ConstraintProto::ConstraintCase::kInterval) {
+    if (type == ConstraintProto::CONSTRAINT_NOT_SET) continue;
+    if (type == ConstraintProto::kDummyConstraint) continue;
+    if (type == ConstraintProto::kInterval) {
       interval_mapping[c] = new_num_constraints;
     }
     context_->working_model->mutable_constraints(new_num_constraints++)
@@ -1279,13 +1279,15 @@ bool CpModelPresolver::PresolveIntMod(ConstraintProto* ct) {
   return false;
 }
 
+// TODO(user): Now that everything has affine relations, we should maybe
+// canonicalize all linear subexpression in an generic way.
 bool CpModelPresolver::ExploitEquivalenceRelations(int c, ConstraintProto* ct) {
   bool changed = false;
 
   // Optim: Special case for the linear constraint. We just remap the
   // enforcement literals, the normal variables will be replaced by their
   // representative in CanonicalizeLinear().
-  if (ct->constraint_case() == ConstraintProto::ConstraintCase::kLinear) {
+  if (ct->constraint_case() == ConstraintProto::kLinear) {
     for (int& ref : *ct->mutable_enforcement_literal()) {
       const int rep = this->context_->GetLiteralRepresentative(ref);
       if (rep != ref) {
@@ -1308,17 +1310,6 @@ bool CpModelPresolver::ExploitEquivalenceRelations(int c, ConstraintProto* ct) {
   }
   if (!work_to_do) return false;
 
-  // Remap equal and negated variables to their representative.
-  ApplyToAllVariableIndices(
-      [&changed, this](int* ref) {
-        const int rep = context_->GetVariableRepresentative(*ref);
-        if (rep != *ref) {
-          changed = true;
-          *ref = rep;
-        }
-      },
-      ct);
-
   // Remap literal and negated literal to their representative.
   ApplyToAllLiteralIndices(
       [&changed, this](int* ref) {
@@ -1461,10 +1452,8 @@ bool CpModelPresolver::CanonicalizeLinearExpression(
 }
 
 bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;
 
   if (ct->linear().domain().empty()) {
     context_->UpdateRuleStats("linear: no domain");
@@ -1484,7 +1473,7 @@ bool CpModelPresolver::CanonicalizeLinear(ConstraintProto* ct) {
 }
 
 bool CpModelPresolver::RemoveSingletonInLinear(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
+  if (ct->constraint_case() != ConstraintProto::kLinear ||
       context_->ModelIsUnsat()) {
     return false;
   }
@@ -2169,9 +2158,7 @@ void TakeIntersectionWith(const absl::flat_hash_set<int>& current,
 
 bool CpModelPresolver::DetectAndProcessOneSidedLinearConstraint(
     int c, ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
   if (context_->ModelIsUnsat()) return false;
   if (context_->keep_all_feasible_solutions) return false;
 
@@ -2290,10 +2277,8 @@ bool CpModelPresolver::DetectAndProcessOneSidedLinearConstraint(
 
 bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
                                                 ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;
 
   // Compute the implied rhs bounds from the variable ones.
   auto& term_domains = context_->tmp_term_domains;
@@ -2469,7 +2454,7 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
       }
       if (c == ct_index) continue;
       if (context_->working_model->constraints(c).constraint_case() !=
-          ConstraintProto::ConstraintCase::kLinear) {
+          ConstraintProto::kLinear) {
         abort = true;
         break;
       }
@@ -2548,10 +2533,8 @@ bool CpModelPresolver::PropagateDomainsInLinear(int ct_index,
 // This operation is similar to coefficient strengthening in the MIP world.
 void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
     int ct_index, ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return;
+  if (context_->ModelIsUnsat()) return;
 
   const LinearConstraintProto& arg = ct->linear();
   const int num_vars = arg.vars_size();
@@ -2624,7 +2607,9 @@ void CpModelPresolver::ExtractEnforcementLiteralFromLinearConstraint(
                       new_ct2->mutable_linear());
 
     context_->UpdateNewConstraintsVariableUsage();
-    return (void)RemoveConstraint(ct);
+    ct->Clear();
+    context_->UpdateConstraintVariableUsage(ct_index);
+    return;
   }
 
   // Any coefficient greater than this will cause the constraint to be trivially
@@ -2751,10 +2736,8 @@ void CpModelPresolver::ExtractAtMostOneFromLinear(ConstraintProto* ct) {
 // Convert some linear constraint involving only Booleans to their Boolean
 // form.
 bool CpModelPresolver::PresolveLinearOnBooleans(ConstraintProto* ct) {
-  if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
-      context_->ModelIsUnsat()) {
-    return false;
-  }
+  if (ct->constraint_case() != ConstraintProto::kLinear) return false;
+  if (context_->ModelIsUnsat()) return false;
 
   const LinearConstraintProto& arg = ct->linear();
   const int num_vars = arg.vars_size();
@@ -4969,7 +4952,7 @@ void CpModelPresolver::ExtractBoolAnd() {
     const ConstraintProto& ct = context_->working_model->constraints(c);
     if (HasEnforcementLiteral(ct)) continue;
 
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr &&
+    if (ct.constraint_case() == ConstraintProto::kBoolOr &&
         ct.bool_or().literals().size() == 2) {
       AddImplication(NegatedRef(ct.bool_or().literals(0)),
                      ct.bool_or().literals(1), context_->working_model,
@@ -4978,7 +4961,7 @@ void CpModelPresolver::ExtractBoolAnd() {
       continue;
     }
 
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne &&
+    if (ct.constraint_case() == ConstraintProto::kAtMostOne &&
         ct.at_most_one().literals().size() == 2) {
       AddImplication(ct.at_most_one().literals(0),
                      NegatedRef(ct.at_most_one().literals(1)),
@@ -5100,8 +5083,8 @@ void CpModelPresolver::PresolvePureSatPart() {
   // reach this point?
   for (int c = 0; c < context_->working_model->constraints_size(); ++c) {
     const ConstraintProto& ct = context_->working_model->constraints(c);
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr ||
-        ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
+    if (ct.constraint_case() == ConstraintProto::kBoolOr ||
+        ct.constraint_case() == ConstraintProto::kBoolAnd) {
       if (PresolveOneConstraint(c)) {
         context_->UpdateConstraintVariableUsage(c);
       }
@@ -5125,7 +5108,7 @@ void CpModelPresolver::PresolvePureSatPart() {
   for (int i = 0; i < context_->working_model->constraints_size(); ++i) {
     const ConstraintProto& ct = context_->working_model->constraints(i);
 
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolOr) {
+    if (ct.constraint_case() == ConstraintProto::kBoolOr) {
       ++num_removed_constraints;
       clause.clear();
       for (const int ref : ct.bool_or().literals()) {
@@ -5141,7 +5124,7 @@ void CpModelPresolver::PresolvePureSatPart() {
       continue;
     }
 
-    if (ct.constraint_case() == ConstraintProto::ConstraintCase::kBoolAnd) {
+    if (ct.constraint_case() == ConstraintProto::kBoolAnd) {
       ++num_removed_constraints;
       std::vector<Literal> clause;
       for (const int ref : ct.enforcement_literal()) {
@@ -5265,7 +5248,7 @@ void CpModelPresolver::ExpandObjective() {
     const ConstraintProto& ct = context_->working_model->constraints(ct_index);
     // Skip everything that is not a linear equality constraint.
     if (!ct.enforcement_literal().empty() ||
-        ct.constraint_case() != ConstraintProto::ConstraintCase::kLinear ||
+        ct.constraint_case() != ConstraintProto::kLinear ||
         ct.linear().domain().size() != 2 ||
         ct.linear().domain(0) != ct.linear().domain(1)) {
       continue;
@@ -5472,9 +5455,7 @@ void CpModelPresolver::MergeNoOverlapConstraints() {
   std::vector<std::vector<Literal>> cliques;
   for (int c = 0; c < num_constraints; ++c) {
     const ConstraintProto& ct = context_->working_model->constraints(c);
-    if (ct.constraint_case() != ConstraintProto::ConstraintCase::kNoOverlap) {
-      continue;
-    }
+    if (ct.constraint_case() != ConstraintProto::kNoOverlap) continue;
     std::vector<Literal> clique;
     for (const int i : ct.no_overlap().intervals()) {
       clique.push_back(Literal(BooleanVariable(i), true));
@@ -5545,7 +5526,7 @@ void CpModelPresolver::TransformIntoMaxCliques() {
 
   for (int c = 0; c < num_constraints; ++c) {
     ConstraintProto* ct = context_->working_model->mutable_constraints(c);
-    if (ct->constraint_case() == ConstraintProto::ConstraintCase::kAtMostOne) {
+    if (ct->constraint_case() == ConstraintProto::kAtMostOne) {
       std::vector<Literal> clique;
       for (const int ref : ct->at_most_one().literals()) {
         clique.push_back(convert(ref));
@@ -5554,8 +5535,7 @@ void CpModelPresolver::TransformIntoMaxCliques() {
       if (RemoveConstraint(ct)) {
         context_->UpdateConstraintVariableUsage(c);
       }
-    } else if (ct->constraint_case() ==
-               ConstraintProto::ConstraintCase::kBoolAnd) {
+    } else if (ct->constraint_case() == ConstraintProto::kBoolAnd) {
       if (ct->enforcement_literal().size() != 1) continue;
       const Literal enforcement = convert(ct->enforcement_literal(0));
       for (const int ref : ct->bool_and().literals()) {
@@ -5679,17 +5659,17 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
 
   // Call the presolve function for this constraint if any.
   switch (ct->constraint_case()) {
-    case ConstraintProto::ConstraintCase::kBoolOr:
+    case ConstraintProto::kBoolOr:
       return PresolveBoolOr(ct);
-    case ConstraintProto::ConstraintCase::kBoolAnd:
+    case ConstraintProto::kBoolAnd:
       return PresolveBoolAnd(ct);
-    case ConstraintProto::ConstraintCase::kAtMostOne:
+    case ConstraintProto::kAtMostOne:
       return PresolveAtMostOne(ct);
-    case ConstraintProto::ConstraintCase::kExactlyOne:
+    case ConstraintProto::kExactlyOne:
       return PresolveExactlyOne(ct);
-    case ConstraintProto::ConstraintCase::kBoolXor:
+    case ConstraintProto::kBoolXor:
       return PresolveBoolXor(ct);
-    case ConstraintProto::ConstraintCase::kLinMax:
+    case ConstraintProto::kLinMax:
       if (CanonicalizeLinearArgument(*ct, ct->mutable_lin_max())) {
         context_->UpdateConstraintVariableUsage(c);
       }
@@ -5698,22 +5678,22 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
       } else {
         return PresolveLinMax(ct);
       }
-    case ConstraintProto::ConstraintCase::kIntProd:
+    case ConstraintProto::kIntProd:
       if (CanonicalizeLinearArgument(*ct, ct->mutable_int_prod())) {
         context_->UpdateConstraintVariableUsage(c);
       }
       return PresolveIntProd(ct);
-    case ConstraintProto::ConstraintCase::kIntDiv:
+    case ConstraintProto::kIntDiv:
       if (CanonicalizeLinearArgument(*ct, ct->mutable_int_div())) {
         context_->UpdateConstraintVariableUsage(c);
       }
       return PresolveIntDiv(ct);
-    case ConstraintProto::ConstraintCase::kIntMod:
+    case ConstraintProto::kIntMod:
       if (CanonicalizeLinearArgument(*ct, ct->mutable_int_mod())) {
         context_->UpdateConstraintVariableUsage(c);
       }
       return PresolveIntMod(ct);
-    case ConstraintProto::ConstraintCase::kLinear: {
+    case ConstraintProto::kLinear: {
       // In the presence of affine relation, it is possible that the sign of a
       // variable change during canonicalization, and a variable that could
       // freely move in one direction can no longer do so. So we make sure we
@@ -5756,16 +5736,15 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
       if (PresolveLinearOnBooleans(ct)) {
         context_->UpdateConstraintVariableUsage(c);
       }
-      if (ct->constraint_case() == ConstraintProto::kLinear) {
-        const int old_num_enforcement_literals = ct->enforcement_literal_size();
-        ExtractEnforcementLiteralFromLinearConstraint(c, ct);
-        if (ct->constraint_case() ==
-            ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
+
+      // If we extracted some enforcement, we redo some preoslve.
+      const int old_num_enforcement_literals = ct->enforcement_literal_size();
+      ExtractEnforcementLiteralFromLinearConstraint(c, ct);
+      if (ct->enforcement_literal_size() > old_num_enforcement_literals) {
+        if (DivideLinearByGcd(ct)) {
           context_->UpdateConstraintVariableUsage(c);
-          return true;
         }
-        if (ct->enforcement_literal_size() > old_num_enforcement_literals &&
-            PresolveSmallLinear(ct)) {
+        if (PresolveSmallLinear(ct)) {
           context_->UpdateConstraintVariableUsage(c);
         }
       }
@@ -5773,35 +5752,34 @@ bool CpModelPresolver::PresolveOneConstraint(int c) {
       // Note that it is important for this to be last, so that if a constraint
       // is marked as being in one direction, no other presolve is applied until
       // it is processed again and unmarked at the beginning of this case.
-      if (ct->constraint_case() == ConstraintProto::kLinear &&
-          DetectAndProcessOneSidedLinearConstraint(c, ct)) {
+      if (DetectAndProcessOneSidedLinearConstraint(c, ct)) {
         context_->UpdateConstraintVariableUsage(c);
       }
       return false;
     }
-    case ConstraintProto::ConstraintCase::kInterval:
+    case ConstraintProto::kInterval:
       return PresolveInterval(c, ct);
-    case ConstraintProto::ConstraintCase::kInverse:
+    case ConstraintProto::kInverse:
       return PresolveInverse(ct);
-    case ConstraintProto::ConstraintCase::kElement:
+    case ConstraintProto::kElement:
       return PresolveElement(ct);
-    case ConstraintProto::ConstraintCase::kTable:
+    case ConstraintProto::kTable:
       return PresolveTable(ct);
-    case ConstraintProto::ConstraintCase::kAllDiff:
+    case ConstraintProto::kAllDiff:
       return PresolveAllDiff(ct);
-    case ConstraintProto::ConstraintCase::kNoOverlap:
+    case ConstraintProto::kNoOverlap:
       return PresolveNoOverlap(ct);
-    case ConstraintProto::ConstraintCase::kNoOverlap2D:
+    case ConstraintProto::kNoOverlap2D:
       return PresolveNoOverlap2D(c, ct);
-    case ConstraintProto::ConstraintCase::kCumulative:
+    case ConstraintProto::kCumulative:
       return PresolveCumulative(ct);
-    case ConstraintProto::ConstraintCase::kCircuit:
+    case ConstraintProto::kCircuit:
       return PresolveCircuit(ct);
-    case ConstraintProto::ConstraintCase::kRoutes:
+    case ConstraintProto::kRoutes:
       return PresolveRoutes(ct);
-    case ConstraintProto::ConstraintCase::kAutomaton:
+    case ConstraintProto::kAutomaton:
       return PresolveAutomaton(ct);
-    case ConstraintProto::ConstraintCase::kReservoir:
+    case ConstraintProto::kReservoir:
       return PresolveReservoir(ct);
     default:
       return false;
@@ -7059,7 +7037,7 @@ void CpModelPresolver::PresolveToFixPoint() {
   std::deque<int> queue;
   for (int c = 0; c < in_queue.size(); ++c) {
     if (context_->working_model->constraints(c).constraint_case() !=
-        ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) {
+        ConstraintProto::CONSTRAINT_NOT_SET) {
       in_queue[c] = true;
       queue.push_back(c);
     }
@@ -7227,25 +7205,25 @@ void CpModelPresolver::PresolveToFixPoint() {
   for (int c = 0; c < num_constraints; ++c) {
     ConstraintProto* ct = context_->working_model->mutable_constraints(c);
     switch (ct->constraint_case()) {
-      case ConstraintProto::ConstraintCase::kNoOverlap:
+      case ConstraintProto::kNoOverlap:
         // Filter out absent intervals.
         if (PresolveNoOverlap(ct)) {
           context_->UpdateConstraintVariableUsage(c);
         }
         break;
-      case ConstraintProto::ConstraintCase::kNoOverlap2D:
+      case ConstraintProto::kNoOverlap2D:
         // Filter out absent intervals.
         if (PresolveNoOverlap2D(c, ct)) {
           context_->UpdateConstraintVariableUsage(c);
         }
         break;
-      case ConstraintProto::ConstraintCase::kCumulative:
+      case ConstraintProto::kCumulative:
         // Filter out absent intervals.
         if (PresolveCumulative(ct)) {
           context_->UpdateConstraintVariableUsage(c);
         }
         break;
-      case ConstraintProto::ConstraintCase::kBoolOr: {
+      case ConstraintProto::kBoolOr: {
         // Try to infer domain reductions from clauses and the saved "implies in
         // domain" relations.
         for (const auto& pair :
@@ -7750,19 +7728,19 @@ CpSolverStatus CpModelPresolver::Presolve() {
       ConstraintProto* ct = context_->working_model->mutable_constraints(c);
       PresolveEnforcementLiteral(ct);
       switch (ct->constraint_case()) {
-        case ConstraintProto::ConstraintCase::kBoolOr:
+        case ConstraintProto::kBoolOr:
           PresolveBoolOr(ct);
           break;
-        case ConstraintProto::ConstraintCase::kBoolAnd:
+        case ConstraintProto::kBoolAnd:
           PresolveBoolAnd(ct);
           break;
-        case ConstraintProto::ConstraintCase::kAtMostOne:
+        case ConstraintProto::kAtMostOne:
           PresolveAtMostOne(ct);
           break;
-        case ConstraintProto::ConstraintCase::kExactlyOne:
+        case ConstraintProto::kExactlyOne:
           PresolveExactlyOne(ct);
           break;
-        case ConstraintProto::ConstraintCase::kLinear:
+        case ConstraintProto::kLinear:
           CanonicalizeLinear(ct);
           break;
         default:
@@ -7822,7 +7800,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
     for (int c = 0; c < context_->working_model->constraints_size(); ++c) {
       const auto type =
           context_->working_model->constraints(c).constraint_case();
-      if (type == ConstraintProto::ConstraintCase::CONSTRAINT_NOT_SET) continue;
+      if (type == ConstraintProto::CONSTRAINT_NOT_SET) continue;
       old_num_non_empty_constraints++;
     }
 
@@ -7868,9 +7846,7 @@ CpSolverStatus CpModelPresolver::Presolve() {
       const int old_size = context_->working_model->constraints_size();
       for (int c = 0; c < old_size; ++c) {
         ConstraintProto* ct = context_->working_model->mutable_constraints(c);
-        if (ct->constraint_case() != ConstraintProto::ConstraintCase::kLinear) {
-          continue;
-        }
+        if (ct->constraint_case() != ConstraintProto::kLinear) continue;
         ExtractAtMostOneFromLinear(ct);
       }
       context_->UpdateNewConstraintsVariableUsage();
@@ -8239,7 +8215,7 @@ std::vector<std::pair<int, int>> FindDuplicateConstraints(
 
     // TODO(user): we could delete duplicate identical interval, but we need
     // to make sure reference to them are updated.
-    if (type == ConstraintProto::ConstraintCase::kInterval) continue;
+    if (type == ConstraintProto::kInterval) continue;
 
     // We ignore names when comparing constraints.
     //
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 07d4665e02..cd4d29b7b5 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -1444,25 +1444,23 @@ void SolveLoadedCpModel(const CpModelProto& model_proto, Model* model) {
   const auto& mapping = *model->GetOrCreate<CpModelMapping>();
   SatSolver::Status status;
   const SatParameters& parameters = *model->GetOrCreate<SatParameters>();
+
   if (parameters.use_probing_search()) {
-    std::vector<BooleanVariable> bool_vars;
-    std::vector<IntegerVariable> int_vars;
-    IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
-    absl::flat_hash_set<BooleanVariable> visited;
-    for (int v = 0; v < model_proto.variables_size(); ++v) {
-      if (mapping.IsBoolean(v)) {
-        const BooleanVariable bool_var = mapping.Literal(v).Variable();
-        if (!visited.contains(bool_var)) {
-          visited.insert(bool_var);
-          bool_vars.push_back(bool_var);
-        }
-      } else {
-        IntegerVariable var = mapping.Integer(v);
-        if (integer_trail->IsFixed(var)) continue;
-        int_vars.push_back(var);
+    ContinuousProber prober(model_proto, model);
+    while (true) {
+      status = prober.Probe();
+      if (status == SatSolver::INFEASIBLE) {
+        shared_response_manager->NotifyThatImprovingProblemIsInfeasible(
+            solution_info);
+        break;
+      }
+      if (status == SatSolver::FEASIBLE) {
+        solution_observer();
+      }
+      if (status == SatSolver::LIMIT_REACHED) {
+        break;
       }
     }
-    status = ContinuousProbing(bool_vars, int_vars, solution_observer, model);
   } else if (!model_proto.has_objective()) {
     while (true) {
       status = ResetAndSolveIntegerProblem(
diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc
index 5b0590273e..37af23ebb3 100644
--- a/ortools/sat/integer_search.cc
+++ b/ortools/sat/integer_search.cc
@@ -16,6 +16,7 @@
 #include <cmath>
 #include <cstdint>
 #include <functional>
+#include <limits>
 #include <vector>
 
 #include "absl/container/flat_hash_set.h"
@@ -1080,130 +1081,227 @@ SatSolver::Status SolveIntegerProblemWithLazyEncoding(Model* model) {
   return ResetAndSolveIntegerProblem(/*assumptions=*/{}, model);
 }
 
-SatSolver::Status ContinuousProbing(
-    const std::vector<BooleanVariable>& bool_vars,
-    const std::vector<IntegerVariable>& int_vars,
-    const std::function<void()>& feasible_solution_observer, Model* model) {
-  VLOG(2) << "Start continuous probing with " << bool_vars.size()
-          << " Boolean variables, and " << int_vars.size()
-          << " integer variables";
-
-  SatSolver* solver = model->GetOrCreate<SatSolver>();
-  TimeLimit* time_limit = model->GetOrCreate<TimeLimit>();
-  IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
-  IntegerEncoder* encoder = model->GetOrCreate<IntegerEncoder>();
-  const SatParameters& sat_parameters = *(model->GetOrCreate<SatParameters>());
-  auto* level_zero_callbacks = model->GetOrCreate<LevelZeroCallbackHelper>();
-  Prober* prober = model->GetOrCreate<Prober>();
-  auto* shared_response_manager = model->Mutable<SharedResponseManager>();
-  auto* shared_bounds_manager = model->Mutable<SharedBoundsManager>();
-
-  std::vector<BooleanVariable> active_vars;
-  std::vector<BooleanVariable> integer_bounds;
-  absl::flat_hash_set<BooleanVariable> integer_bounds_set;
-
-  int iteration = 1;
-  absl::Time last_check = absl::Now();
-
-  while (!time_limit->LimitReached()) {
-    if (shared_response_manager != nullptr &&
-        shared_bounds_manager != nullptr &&
-        absl::Now() - last_check >= absl::Seconds(10)) {
-      shared_response_manager->LogMessage(
-          "Probe",
-          absl::StrCat("#iterations:", iteration,
-                       " #literals_fixed:", prober->num_new_literals_fixed(),
-                       " #new_integer_bounds:",
-                       shared_bounds_manager->NumBoundsExported("probing")));
-      last_check = absl::Now();
-    }
-    iteration++;
-
-    // Sync the bounds first.
-    auto SyncBounds = [solver, &level_zero_callbacks]() {
-      if (!solver->ResetToLevelZero()) return false;
-      for (const auto& cb : level_zero_callbacks->callbacks) {
-        if (!cb()) {
-          solver->NotifyThatModelIsUnsat();
-          return false;
-        }
+ContinuousProber::ContinuousProber(const CpModelProto& model_proto,
+                                   Model* model)
+    : model_(model),
+      sat_solver_(model->GetOrCreate<SatSolver>()),
+      time_limit_(model->GetOrCreate<TimeLimit>()),
+      trail_(model->GetOrCreate<Trail>()),
+      integer_trail_(model->GetOrCreate<IntegerTrail>()),
+      encoder_(model->GetOrCreate<IntegerEncoder>()),
+      sat_parameters_(*(model->GetOrCreate<SatParameters>())),
+      deterministic_time_(sat_parameters_.shaving_search_deterministic_time()),
+      use_shaving_(sat_parameters_.use_shaving_in_probing_search()),
+      level_zero_callbacks_(model->GetOrCreate<LevelZeroCallbackHelper>()),
+      prober_(model->GetOrCreate<Prober>()),
+      shared_response_manager_(model->Mutable<SharedResponseManager>()),
+      shared_bounds_manager_(model->Mutable<SharedBoundsManager>()),
+      active_limit_(deterministic_time_) {
+  auto* mapping = model_->GetOrCreate<CpModelMapping>();
+  absl::flat_hash_set<BooleanVariable> visited;
+  for (int v = 0; v < model_proto.variables_size(); ++v) {
+    if (mapping->IsBoolean(v)) {
+      const BooleanVariable bool_var = mapping->Literal(v).Variable();
+      const auto [_, inserted] = visited.insert(bool_var);
+      if (inserted) {
+        bool_vars_.push_back(bool_var);
       }
-      return true;
-    };
-    if (!SyncBounds()) {
-      return SatSolver::INFEASIBLE;
+    } else {
+      IntegerVariable var = mapping->Integer(v);
+      if (integer_trail_->IsFixed(var)) continue;
+      int_vars_.push_back(var);
     }
+  }
+  VLOG(2) << "Start continuous probing with " << bool_vars_.size()
+          << " Boolean variables, and " << int_vars_.size()
+          << " integer variables"
+          << ", deterministic time limit = "
+          << time_limit_->GetDeterministicLimit() << " on " << model_->Name();
+  last_check_ = absl::Now();
+}
 
+// Continuous probing procedure.
+// TODO(user):
+//   - sort variables before the iteration (statically or dynamically)
+//   - compress clause databases regularly (especially the implication graph)
+//   - better interleaving of the probing and shaving phases
+//   - move the shaving code directly in the probing class
+SatSolver::Status ContinuousProber::Probe() {
+  while (!time_limit_->LimitReached()) {
     // Run sat in-processing to reduce the size of the clause database.
-    if (sat_parameters.use_sat_inprocessing() &&
-        !model->GetOrCreate<Inprocessing>()->InprocessingRound()) {
+    if (sat_parameters_.use_sat_inprocessing() &&
+        !model_->GetOrCreate<Inprocessing>()->InprocessingRound()) {
       return SatSolver::INFEASIBLE;
     }
 
-    // TODO(user): Explore fast probing methods.
-
     // Probe each Boolean variable at most once per loop.
-    absl::flat_hash_set<BooleanVariable> probed;
+    probed_bool_vars_.clear();
+    probed_literals_.clear();
+
+    // Store current statistics to detect an iteration without any improvement.
+    const int64_t initial_num_literals_fixed =
+        prober_->num_new_literals_fixed();
+    const int64_t initial_num_bounds_shaved = num_bounds_shaved_;
 
     // Probe variable bounds.
     // TODO(user): Probe optional variables.
-    for (const IntegerVariable int_var : int_vars) {
-      if (integer_trail->IsFixed(int_var) ||
-          integer_trail->IsOptional(int_var)) {
+    for (const IntegerVariable int_var : int_vars_) {
+      if (integer_trail_->IsFixed(int_var) ||
+          integer_trail_->IsOptional(int_var)) {
         continue;
       }
 
+      if (!ImportFromSharedClasses()) {
+        return SatSolver::INFEASIBLE;
+      }
+
+      if (time_limit_->LimitReached()) {
+        return SatSolver::LIMIT_REACHED;
+      }
+
       const BooleanVariable shave_lb =
-          encoder
+          encoder_
               ->GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(
-                  int_var, integer_trail->LowerBound(int_var)))
+                  int_var, integer_trail_->LowerBound(int_var)))
               .Variable();
-      if (!probed.contains(shave_lb)) {
-        probed.insert(shave_lb);
-        if (!prober->ProbeOneVariable(shave_lb)) {
+      const auto [_lb, lb_inserted] = probed_bool_vars_.insert(shave_lb);
+      if (lb_inserted) {
+        if (!prober_->ProbeOneVariable(shave_lb)) {
           return SatSolver::INFEASIBLE;
         }
+        num_literals_probed_++;
       }
 
       const BooleanVariable shave_ub =
-          encoder
+          encoder_
               ->GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(
-                  int_var, integer_trail->UpperBound(int_var)))
+                  int_var, integer_trail_->UpperBound(int_var)))
               .Variable();
-      if (!probed.contains(shave_ub)) {
-        probed.insert(shave_ub);
-        if (!prober->ProbeOneVariable(shave_ub)) {
+      const auto [_ub, ub_inserted] = probed_bool_vars_.insert(shave_ub);
+      if (ub_inserted) {
+        if (!prober_->ProbeOneVariable(shave_ub)) {
           return SatSolver::INFEASIBLE;
         }
+        num_literals_probed_++;
       }
 
-      if (!SyncBounds()) {
-        return SatSolver::INFEASIBLE;
-      }
-      if (time_limit->LimitReached()) {
-        return SatSolver::LIMIT_REACHED;
+      if (use_shaving_) {
+        const SatSolver::Status lb_status =
+            ShaveLiteral(Literal(shave_lb, true));
+        if (ReportStatus(lb_status)) return lb_status;
+
+        const SatSolver::Status ub_status =
+            ShaveLiteral(Literal(shave_ub, true));
+        if (ReportStatus(ub_status)) return ub_status;
       }
+
+      LogStatistics();
     }
 
     // Probe Boolean variables from the model.
-    for (const BooleanVariable& bool_var : bool_vars) {
-      if (solver->Assignment().VariableIsAssigned(bool_var)) continue;
-      if (time_limit->LimitReached()) {
-        return SatSolver::LIMIT_REACHED;
-      }
-      if (!SyncBounds()) {
+    for (const BooleanVariable& bool_var : bool_vars_) {
+      if (sat_solver_->Assignment().VariableIsAssigned(bool_var)) continue;
+
+      if (!ImportFromSharedClasses()) {
         return SatSolver::INFEASIBLE;
       }
-      if (!probed.contains(bool_var)) {
-        probed.insert(bool_var);
-        if (!prober->ProbeOneVariable(bool_var)) {
+
+      if (time_limit_->LimitReached()) {
+        return SatSolver::LIMIT_REACHED;
+      }
+
+      const auto [_, inserted] = probed_bool_vars_.insert(bool_var);
+      if (inserted) {
+        if (!prober_->ProbeOneVariable(bool_var)) {
           return SatSolver::INFEASIBLE;
         }
+        num_literals_probed_++;
       }
+
+      const Literal literal(bool_var, true);
+      if (use_shaving_ &&
+          !sat_solver_->Assignment().LiteralIsAssigned(literal)) {
+        const SatSolver::Status true_status = ShaveLiteral(literal);
+        if (ReportStatus(true_status)) return true_status;
+        if (true_status == SatSolver::ASSUMPTIONS_UNSAT) continue;
+
+        const SatSolver::Status false_status = ShaveLiteral(literal.Negated());
+        if (ReportStatus(false_status)) return false_status;
+      }
+
+      LogStatistics();
     }
+
+    // Adjust the active_limit.
+    const bool something_has_been_detected =
+        num_bounds_shaved_ != initial_num_bounds_shaved ||
+        prober_->num_new_literals_fixed() != initial_num_literals_fixed;
+    if (something_has_been_detected) {  // Reset the limit.
+      active_limit_ = deterministic_time_;
+    } else if (active_limit_ < 10 * deterministic_time_) {  // Bump the limit.
+      active_limit_ += deterministic_time_;
+    }
+
+    ++iteration_;
   }
   return SatSolver::LIMIT_REACHED;
 }
 
+bool ContinuousProber::ImportFromSharedClasses() {
+  if (!sat_solver_->ResetToLevelZero()) return false;
+  for (const auto& cb : level_zero_callbacks_->callbacks) {
+    if (!cb()) {
+      sat_solver_->NotifyThatModelIsUnsat();
+      return false;
+    }
+  }
+  return true;
+}
+
+SatSolver::Status ContinuousProber::ShaveLiteral(Literal literal) {
+  const auto [_, inserted] = probed_literals_.insert(literal.Index());
+  if (trail_->Assignment().LiteralIsAssigned(literal) || !inserted) {
+    return SatSolver::LIMIT_REACHED;
+  }
+  num_bounds_tried_++;
+
+  const double original_dtime_limit = time_limit_->GetDeterministicLimit();
+  time_limit_->ChangeDeterministicLimit(
+      std::min(original_dtime_limit,
+               time_limit_->GetElapsedDeterministicTime() + active_limit_));
+  const SatSolver::Status status =
+      ResetAndSolveIntegerProblem({literal}, model_);
+  time_limit_->ChangeDeterministicLimit(original_dtime_limit);
+
+  if (status == SatSolver::ASSUMPTIONS_UNSAT) {
+    num_bounds_shaved_++;
+  }
+
+  return status;
+}
+
+bool ContinuousProber::ReportStatus(const SatSolver::Status status) {
+  return status == SatSolver::INFEASIBLE || status == SatSolver::FEASIBLE;
+}
+
+void ContinuousProber::LogStatistics() {
+  if (shared_response_manager_ == nullptr ||
+      shared_bounds_manager_ == nullptr) {
+    return;
+  }
+  const absl::Time now = absl::Now();
+  if (now <= last_check_ + absl::Seconds(10)) return;
+  shared_response_manager_->LogMessage(
+      "Probe",
+      absl::StrCat(
+          "#iterations:", iteration_,
+          " #literals fixed/probed:", prober_->num_new_literals_fixed(), "/",
+          num_literals_probed_, " #bounds shaved/tried:", num_bounds_shaved_,
+          "/", num_bounds_tried_, " #new_integer_bounds:",
+          shared_bounds_manager_->NumBoundsExported("probing"),
+          ", #new_binary_clauses:", prober_->num_new_binary_clauses()));
+  last_check_ = now;
+}
+
 }  // namespace sat
 }  // namespace operations_research
diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h
index f8ef487094..5d606d77f6 100644
--- a/ortools/sat/integer_search.h
+++ b/ortools/sat/integer_search.h
@@ -25,8 +25,10 @@
 
 #include <vector>
 
+#include "ortools/sat/cp_model_mapping.h"
 #include "ortools/sat/integer.h"
 #include "ortools/sat/linear_programming_constraint.h"
+#include "ortools/sat/probing.h"
 #include "ortools/sat/pseudo_costs.h"
 #include "ortools/sat/sat_base.h"
 #include "ortools/sat/sat_solver.h"
@@ -231,8 +233,7 @@ std::vector<std::function<BooleanOrIntegerLiteral()>> CompleteHeuristics(
 // of integer variables.
 SatSolver::Status ContinuousProbing(
     const std::vector<BooleanVariable>& bool_vars,
-    const std::vector<IntegerVariable>& int_vars,
-    const std::function<void()>& feasible_solution_observer, Model* model);
+    const std::vector<IntegerVariable>& int_vars, Model* model);
 
 // An helper class to share the code used by the different kind of search.
 class IntegerSearchHelper {
@@ -262,6 +263,46 @@ class IntegerSearchHelper {
   IntegerVariable objective_var_ = kNoIntegerVariable;
 };
 
+// This class will loop continuously on model variables and try to probe/shave
+// its bounds.
+class ContinuousProber {
+ public:
+  ContinuousProber(const CpModelProto& model_proto, Model* model);
+  SatSolver::Status Probe();
+
+ private:
+  bool ImportFromSharedClasses();
+  SatSolver::Status ShaveLiteral(Literal literal);
+  bool ReportStatus(const SatSolver::Status status);
+  void LogStatistics();
+
+  std::vector<BooleanVariable> bool_vars_;
+  std::vector<IntegerVariable> int_vars_;
+  Model* model_;
+  SatSolver* sat_solver_;
+  TimeLimit* time_limit_;
+  Trail* trail_;
+  IntegerTrail* integer_trail_;
+  IntegerEncoder* encoder_;
+  const SatParameters sat_parameters_;
+  const double deterministic_time_;
+  const bool use_shaving_;
+  LevelZeroCallbackHelper* level_zero_callbacks_;
+  Prober* prober_;
+  SharedResponseManager* shared_response_manager_;
+  SharedBoundsManager* shared_bounds_manager_;
+  double active_limit_;
+  int64_t num_bounds_shaved_ = 0;
+  int64_t num_bounds_tried_ = 0;
+  // Probe each Boolean variable or literal at most once per loop.
+  // TODO(user): use 2 vector<bool>.
+  absl::flat_hash_set<BooleanVariable> probed_bool_vars_;
+  absl::flat_hash_set<LiteralIndex> probed_literals_;
+  int iteration_ = 1;
+  int64_t num_literals_probed_ = 0;
+  absl::Time last_check_;
+};
+
 }  // namespace sat
 }  // namespace operations_research
 
diff --git a/ortools/sat/pb_constraint.h b/ortools/sat/pb_constraint.h
index 017a080206..50b250d03a 100644
--- a/ortools/sat/pb_constraint.h
+++ b/ortools/sat/pb_constraint.h
@@ -571,6 +571,7 @@ class PbConstraints : public SatPropagator {
 
   // Returns the number of constraints managed by this class.
   int NumberOfConstraints() const { return constraints_.size(); }
+  bool IsEmpty() const final { return constraints_.empty(); }
 
   // ConflictingConstraint() returns the last PB constraint that caused a
   // conflict. Calling ClearConflictingConstraint() reset this to nullptr.
diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h
index 0e36cd5a2b..003f67d34a 100644
--- a/ortools/sat/probing.h
+++ b/ortools/sat/probing.h
@@ -76,6 +76,7 @@ class Prober {
   // They are reset each time ProbleBooleanVariables() is called.
   // Note however that we do not reset them on a call to ProbeOneVariable().
   int num_new_literals_fixed() const { return num_new_literals_fixed_; }
+  int num_new_binary_clauses() const { return num_new_binary_; }
 
  private:
   bool ProbeOneVariableInternal(BooleanVariable b);
diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h
index 8eb9a23f26..a333de11c5 100644
--- a/ortools/sat/sat_base.h
+++ b/ortools/sat/sat_base.h
@@ -503,6 +503,12 @@ class SatPropagator {
     return propagation_trail_index_ == trail.Index();
   }
 
+  // Small optimization: If a propagator does not contain any "constraints"
+  // there is no point calling propagate on it. Before each propagation, the
+  // solver will checks for emptiness, and construct an optimized list of
+  // propagator before looping many time over the list.
+  virtual bool IsEmpty() const { return false; }
+
  protected:
   const std::string name_;
   int propagator_id_;
diff --git a/ortools/sat/sat_parameters.proto b/ortools/sat/sat_parameters.proto
index 12a33e29d4..ede79823d5 100644
--- a/ortools/sat/sat_parameters.proto
+++ b/ortools/sat/sat_parameters.proto
@@ -24,7 +24,7 @@ option csharp_namespace = "Google.OrTools.Sat";
 // Contains the definitions for all the sat algorithm parameters and their
 // default values.
 //
-// NEXT TAG: 204
+// NEXT TAG: 206
 message SatParameters {
   // In some context, like in a portfolio of search, it makes sense to name a
   // given parameters set for logging purpose.
@@ -826,9 +826,18 @@ message SatParameters {
   optional int64 probing_period_at_root = 142 [default = 0];
 
   // If true, search will continuously probe Boolean variables, and integer
-  // variable bounds.
+  // variable bounds. This parameter is set to true in parallel on the probing
+  // worker.
   optional bool use_probing_search = 176 [default = false];
 
+  // Add a shaving phase (where the solver tries to prove that the lower or
+  // upper bound of a variable are infeasible) to the probing search.
+  optional bool use_shaving_in_probing_search = 204 [default = true];
+
+  // Specifies the amount of deterministic time spent of each try at shaving a
+  // bound in the shaving search.
+  optional double shaving_search_deterministic_time = 205 [default = 0.001];
+
   // The solver ignores the pseudo costs of variables with number of recordings
   // less than this threshold.
   optional int64 pseudo_cost_reliability_threshold = 123 [default = 100];
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index 4c032b420b..72cc49740e 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -1617,17 +1617,29 @@ void SatSolver::ProcessNewlyFixedVariables() {
   deterministic_time_of_last_fixed_variables_cleanup_ = deterministic_time();
 }
 
+bool SatSolver::PropagationIsDone() const {
+  for (SatPropagator* propagator : propagators_) {
+    if (propagator->IsEmpty()) continue;
+    if (!propagator->PropagationIsDone(*trail_)) return false;
+  }
+  return true;
+}
+
 // TODO(user): Support propagating only the "first" propagators. That can
 // be useful for probing/in-processing, so we can control if we do only the SAT
 // part or the full integer part...
 bool SatSolver::Propagate() {
   SCOPED_TIME_STAT(&stats_);
 
-  // If new binary or pb constraint were added for the first time, we need
-  // to "re-initialize" the list of propagators.
-  if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
-      (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
-    InitializePropagators();
+  // Because we might potentially iterate often on this list below, we remove
+  // empty propagators.
+  //
+  // TODO(user): This might not really be needed.
+  non_empty_propagators_.clear();
+  for (SatPropagator* propagator : propagators_) {
+    if (!propagator->IsEmpty()) {
+      non_empty_propagators_.push_back(propagator);
+    }
   }
 
   while (true) {
@@ -1639,7 +1651,7 @@ bool SatSolver::Propagate() {
     // and that its Propagate() functions will not abort on the first
     // propagation to be slightly more efficient.
     const int old_index = trail_->Index();
-    for (SatPropagator* propagator : propagators_) {
+    for (SatPropagator* propagator : non_empty_propagators_) {
       DCHECK(propagator->PropagatePreconditionsAreSatisfied(*trail_));
       if (!propagator->Propagate(trail_)) return false;
       if (trail_->Index() > old_index) break;
@@ -1651,24 +1663,9 @@ bool SatSolver::Propagate() {
 
 void SatSolver::InitializePropagators() {
   propagators_.clear();
-
-  // To make Propagate() as fast as possible, we only add the
-  // binary_implication_graph_/pb_constraints_ propagators if there is anything
-  // to propagate.
-  //
-  // TODO(user): uses the Model classes here to only call
-  // model.GetOrCreate<BinaryImplicationGraph>() when the first binary
-  // constraint is needed, and have a mecanism to always make this propagator
-  // first. Same for the linear constraints.
-  if (!binary_implication_graph_->IsEmpty()) {
-    propagate_binary_ = true;
-    propagators_.push_back(binary_implication_graph_);
-  }
+  propagators_.push_back(binary_implication_graph_);
   propagators_.push_back(clauses_propagator_);
-  if (pb_constraints_->NumberOfConstraints() > 0) {
-    propagate_pb_ = true;
-    propagators_.push_back(pb_constraints_);
-  }
+  propagators_.push_back(pb_constraints_);
   for (int i = 0; i < external_propagators_.size(); ++i) {
     propagators_.push_back(external_propagators_[i]);
   }
@@ -1677,13 +1674,6 @@ void SatSolver::InitializePropagators() {
   }
 }
 
-bool SatSolver::PropagationIsDone() const {
-  for (SatPropagator* propagator : propagators_) {
-    if (!propagator->PropagationIsDone(*trail_)) return false;
-  }
-  return true;
-}
-
 bool SatSolver::ResolvePBConflict(BooleanVariable var,
                                   MutableUpperBoundedLinearConstraint* conflict,
                                   Coefficient* slack) {
@@ -1768,13 +1758,8 @@ void SatSolver::EnqueueNewDecision(Literal literal) {
 void SatSolver::Untrail(int target_trail_index) {
   SCOPED_TIME_STAT(&stats_);
   DCHECK_LT(target_trail_index, trail_->Index());
-
-  if ((!propagate_binary_ && !binary_implication_graph_->IsEmpty()) ||
-      (!propagate_pb_ && pb_constraints_->NumberOfConstraints() > 0)) {
-    InitializePropagators();
-  }
-
   for (SatPropagator* propagator : propagators_) {
+    if (propagator->IsEmpty()) continue;
     propagator->Untrail(*trail_, target_trail_index);
   }
   decision_policy_->Untrail(target_trail_index);
diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h
index 9ebd280056..08e8e3c347 100644
--- a/ortools/sat/sat_solver.h
+++ b/ortools/sat/sat_solver.h
@@ -699,14 +699,13 @@ class SatSolver {
 
   // Internal propagators. We keep them here because we need more than the
   // SatPropagator interface for them.
-  bool propagate_binary_ = false;
-  bool propagate_pb_ = false;
   BinaryImplicationGraph* binary_implication_graph_;
   LiteralWatchers* clauses_propagator_;
   PbConstraints* pb_constraints_;
 
   // Ordered list of propagators used by Propagate()/Untrail().
   std::vector<SatPropagator*> propagators_;
+  std::vector<SatPropagator*> non_empty_propagators_;
 
   // Ordered list of propagators added with AddPropagator().
   std::vector<SatPropagator*> external_propagators_;