diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc
index a08746709c..1e8db35ba4 100644
--- a/ortools/sat/precedences.cc
+++ b/ortools/sat/precedences.cc
@@ -725,6 +725,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
 
       const int old_level = solver->CurrentDecisionLevel();
       solver->EnqueueDecisionAndBacktrackOnConflict(literal.Negated());
+      if (solver->IsModelUnsat()) return;
       const int new_level = solver->CurrentDecisionLevel();
       if (new_level <= old_level) {
         clause = solver->GetLastIncompatibleDecisions();
@@ -756,7 +757,7 @@ void PrecedencesPropagator::AddGreaterThanAtLeastOneOfConstraints(
         selectors.push_back(Literal(arcs_[a].presence_literals.front()));
       }
       model->Add(GreaterThanAtLeastOneOf(target, vars, offsets, selectors));
-      solver->Propagate();
+      if (!solver->FinishPropagation()) return;
     }
   }
 
diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc
index 2c8b988fd0..d449cd2d38 100644
--- a/ortools/sat/sat_solver.cc
+++ b/ortools/sat/sat_solver.cc
@@ -1005,7 +1005,14 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
     moved_last.insert(candidate.back().Index());
   }
 
+  // Returns if we don't have any minimization.
   Backtrack(0);
+  if (candidate.size() == clause->Size()) return;
+
+  // Write the new clause to the proof before the deletion of the old one
+  // happens (when we will detach it).
+  if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
+
   if (candidate.size() == 1) {
     if (!Assignment().VariableIsAssigned(candidate[0].Variable())) {
       counters_.minimization_num_removed_literals += clause->Size();
@@ -1018,21 +1025,17 @@ void SatSolver::TryToMinimizeClause(SatClause* clause) {
     counters_.minimization_num_removed_literals += clause->Size() - 2;
     AddBinaryClauseInternal(candidate[0], candidate[1]);
     clauses_propagator_.Detach(clause);
-    if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
     return;
   }
 
-  if (candidate.size() < clause->Size()) {
-    counters_.minimization_num_removed_literals +=
-        clause->Size() - candidate.size();
+  counters_.minimization_num_removed_literals +=
+      clause->Size() - candidate.size();
 
-    // TODO(user): If the watched literal didn't change, we could just rewrite
-    // the clause while keeping the two watched literals at the beginning.
-    clauses_propagator_.Detach(clause);
-    clause->Rewrite(candidate);
-    clauses_propagator_.Attach(clause, trail_);
-    if (drat_writer_ != nullptr) drat_writer_->AddClause(candidate);
-  }
+  // TODO(user): If the watched literal didn't change, we could just rewrite
+  // the clause while keeping the two watched literals at the beginning.
+  clauses_propagator_.Detach(clause);
+  clause->Rewrite(candidate);
+  clauses_propagator_.Attach(clause, trail_);
 }
 
 SatSolver::Status SatSolver::SolveInternal(TimeLimit* time_limit) {
@@ -1471,6 +1474,17 @@ void SatSolver::ProcessNewlyFixedVariables() {
   int num_detached_clauses = 0;
   int num_binary = 0;
 
+  if (drat_writer_ != nullptr) {
+    // We need to output the literals that are fixed so we can remove all
+    // clauses that contains them. Note that this doesn't seems to be needed
+    // for drat-trim.
+    Literal temp;
+    for (int i = num_processed_fixed_variables_; i < trail_->Index(); ++i) {
+      temp = (*trail_)[i];
+      drat_writer_->AddClause({&temp, 1});
+    }
+  }
+
   // We remove the clauses that are always true and the fixed literals from the
   // others. Note that none of the clause should be all false because we should
   // have detected a conflict before this is called.
@@ -1483,26 +1497,26 @@ void SatSolver::ProcessNewlyFixedVariables() {
       clauses_propagator_.LazyDetach(clause);
       ++num_detached_clauses;
       continue;
-    } else if (clause->Size() != old_size) {
-      if (clause->Size() == 2 &&
-          parameters_->treat_binary_clauses_separately()) {
-        // 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());
-        clauses_propagator_.LazyDetach(clause);
-        ++num_binary;
-        continue;
-      }
     }
 
     const size_t new_size = clause->Size();
-    if (new_size != old_size && drat_writer_ != nullptr) {
+    if (new_size == old_size) continue;
+
+    if (drat_writer_ != nullptr) {
       CHECK_GT(new_size, 0);
       drat_writer_->AddClause({clause->begin(), new_size});
       drat_writer_->DeleteClause({clause->begin(), old_size});
     }
+
+    if (new_size == 2 && parameters_->treat_binary_clauses_separately()) {
+      // 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());
+      clauses_propagator_.LazyDetach(clause);
+      ++num_binary;
+      continue;
+    }
   }
 
   // Note that we will only delete the clauses during the next database cleanup.
diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc
index e58ce46b79..8c661a3aa0 100644
--- a/ortools/sat/simplification.cc
+++ b/ortools/sat/simplification.cc
@@ -161,13 +161,15 @@ void SatPresolver::AddClause(absl::Span<Literal> clause) {
   in_clause_to_process_.push_back(true);
   clause_to_process_.push_back(ci);
 
+  bool changed = false;
   std::vector<Literal>& clause_ref = clauses_.back();
   if (!equiv_mapping_.empty()) {
     for (int i = 0; i < clause_ref.size(); ++i) {
+      const Literal old_literal = clause_ref[i];
       clause_ref[i] = Literal(equiv_mapping_[clause_ref[i].Index()]);
+      if (old_literal != clause_ref[i]) changed = true;
     }
   }
-  const int old_size = clause_ref.size();
   std::sort(clause_ref.begin(), clause_ref.end());
   clause_ref.erase(std::unique(clause_ref.begin(), clause_ref.end()),
                    clause_ref.end());
@@ -184,7 +186,7 @@ void SatPresolver::AddClause(absl::Span<Literal> clause) {
     }
   }
 
-  if (drat_writer_ != nullptr && clause_ref.size() < old_size) {
+  if (drat_writer_ != nullptr && changed) {
     drat_writer_->AddClause(clause_ref);
     drat_writer_->DeleteClause(clause);
   }