diff --git a/ortools/flatzinc/cp_model_fz_solver.cc b/ortools/flatzinc/cp_model_fz_solver.cc
index a2eaea69fa..cd4389f266 100644
--- a/ortools/flatzinc/cp_model_fz_solver.cc
+++ b/ortools/flatzinc/cp_model_fz_solver.cc
@@ -403,7 +403,7 @@ void CpModelProtoWithMapping::FillConstraint(const fz::Constraint& fz_ct,
     for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
     for (const int64 value : fz_ct.arguments[1].values) arg->add_values(value);
   } else if (fz_ct.type == "regular") {
-    auto* arg = ct->mutable_automata();
+    auto* arg = ct->mutable_automaton();
     for (const int var : LookupVars(fz_ct.arguments[0])) arg->add_vars(var);
 
     int count = 0;
diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc
index ad981b9676..18ba051ba7 100644
--- a/ortools/sat/cp_model.cc
+++ b/ortools/sat/cp_model.cc
@@ -233,9 +233,9 @@ void ReservoirConstraint::AddOptionalEvent(IntVar time, int64 demand,
 
 void AutomatonConstraint::AddTransition(int tail, int head,
                                         int64 transition_label) {
-  proto_->mutable_automata()->add_transition_tail(tail);
-  proto_->mutable_automata()->add_transition_head(head);
-  proto_->mutable_automata()->add_transition_label(transition_label);
+  proto_->mutable_automaton()->add_transition_tail(tail);
+  proto_->mutable_automaton()->add_transition_head(head);
+  proto_->mutable_automaton()->add_transition_label(transition_label);
 }
 
 void NoOverlap2DConstraint::AddRectangle(IntervalVar x_coordinate,
@@ -584,11 +584,11 @@ AutomatonConstraint CpModelBuilder::AddAutomaton(
     absl::Span<const int> final_states) {
   ConstraintProto* const proto = cp_model_.add_constraints();
   for (const IntVar& var : transition_variables) {
-    proto->mutable_automata()->add_vars(GetOrCreateIntegerIndex(var.index_));
+    proto->mutable_automaton()->add_vars(GetOrCreateIntegerIndex(var.index_));
   }
-  proto->mutable_automata()->set_starting_state(starting_state);
+  proto->mutable_automaton()->set_starting_state(starting_state);
   for (const int final_state : final_states) {
-    proto->mutable_automata()->add_final_states(final_state);
+    proto->mutable_automaton()->add_final_states(final_state);
   }
   return AutomatonConstraint(proto);
 }
diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h
index 6bfab9e779..fef63f6d76 100644
--- a/ortools/sat/cp_model.h
+++ b/ortools/sat/cp_model.h
@@ -576,7 +576,7 @@ class CpModelBuilder {
   // and 'label' is the label of an arc from 'head' to 'tail',
   // corresponding to the value of one variable in the list of variables.
   //
-  // This automata will be unrolled into a flow with n + 1 phases. Each phase
+  // This automaton will be unrolled into a flow with n + 1 phases. Each phase
   // contains the possible states of the automaton. The first state contains the
   // initial state. The last phase contains the final states.
   //
diff --git a/ortools/sat/cp_model.proto b/ortools/sat/cp_model.proto
index c42b1d17a6..115e73df19 100644
--- a/ortools/sat/cp_model.proto
+++ b/ortools/sat/cp_model.proto
@@ -222,10 +222,11 @@ message InverseConstraintProto {
   repeated int32 f_inverse = 2;
 }
 
-// This constraint forces a sequence of variables to be accepted by an automata.
-message AutomataConstraintProto {
+// This constraint forces a sequence of variables to be accepted by an
+// automaton.
+message AutomatonConstraintProto {
   // A state is identified by a non-negative number. It is preferable to keep
-  // all the states dense in says [0, num_states). The automata starts at
+  // all the states dense in says [0, num_states). The automaton starts at
   // starting_state and must finish in any of the final states.
   int64 starting_state = 2;
   repeated int64 final_states = 3;
@@ -237,7 +238,7 @@ message AutomataConstraintProto {
   repeated int64 transition_head = 5;
   repeated int64 transition_label = 6;
 
-  // The sequence of variables. The automata is ran for vars_size() "steps" and
+  // The sequence of variables. The automaton is ran for vars_size() "steps" and
   // the value of vars[i] corresponds to the transition label at step i.
   repeated int32 vars = 7;
 }
@@ -330,9 +331,9 @@ message ConstraintProto {
     // take.
     TableConstraintProto table = 16;
 
-    // The automata constraint forces a sequence of variables to be accepted
+    // The automaton constraint forces a sequence of variables to be accepted
     // by an automaton.
-    AutomataConstraintProto automata = 17;
+    AutomatonConstraintProto automaton = 17;
 
     // The inverse constraint forces two arrays to be inverses of each other:
     // the values of one are the indices of the other, and vice versa.
diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc
index ecf2bd4554..9f42f36039 100644
--- a/ortools/sat/cp_model_checker.cc
+++ b/ortools/sat/cp_model_checker.cc
@@ -497,22 +497,22 @@ class ConstraintChecker {
     return ct.table().negated();
   }
 
-  bool AutomataConstraintIsFeasible(const ConstraintProto& ct) {
+  bool AutomatonConstraintIsFeasible(const ConstraintProto& ct) {
     // Build the transition table {tail, label} -> head.
     absl::flat_hash_map<std::pair<int64, int64>, int64> transition_map;
-    const int num_transitions = ct.automata().transition_tail().size();
+    const int num_transitions = ct.automaton().transition_tail().size();
     for (int i = 0; i < num_transitions; ++i) {
-      transition_map[{ct.automata().transition_tail(i),
-                      ct.automata().transition_label(i)}] =
-          ct.automata().transition_head(i);
+      transition_map[{ct.automaton().transition_tail(i),
+                      ct.automaton().transition_label(i)}] =
+          ct.automaton().transition_head(i);
     }
 
-    // Walk the automata.
-    int64 current_state = ct.automata().starting_state();
-    const int num_steps = ct.automata().vars_size();
+    // Walk the automaton.
+    int64 current_state = ct.automaton().starting_state();
+    const int num_steps = ct.automaton().vars_size();
     for (int i = 0; i < num_steps; ++i) {
       const std::pair<int64, int64> key = {current_state,
-                                           Value(ct.automata().vars(i))};
+                                           Value(ct.automaton().vars(i))};
       if (!gtl::ContainsKey(transition_map, key)) {
         return false;
       }
@@ -520,7 +520,7 @@ class ConstraintChecker {
     }
 
     // Check we are now in a final state.
-    for (const int64 final : ct.automata().final_states()) {
+    for (const int64 final : ct.automaton().final_states()) {
       if (current_state == final) return true;
     }
     return false;
@@ -782,8 +782,8 @@ bool SolutionIsFeasible(const CpModelProto& model,
       case ConstraintProto::ConstraintCase::kTable:
         is_feasible = checker.TableConstraintIsFeasible(ct);
         break;
-      case ConstraintProto::ConstraintCase::kAutomata:
-        is_feasible = checker.AutomataConstraintIsFeasible(ct);
+      case ConstraintProto::ConstraintCase::kAutomaton:
+        is_feasible = checker.AutomatonConstraintIsFeasible(ct);
         break;
       case ConstraintProto::ConstraintCase::kCircuit:
         is_feasible = checker.CircuitConstraintIsFeasible(ct);
diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc
index 7ffe760d41..df74da50c9 100644
--- a/ortools/sat/cp_model_loader.cc
+++ b/ortools/sat/cp_model_loader.cc
@@ -1061,23 +1061,23 @@ void LoadTableConstraint(const ConstraintProto& ct, Model* m) {
   }
 }
 
-void LoadAutomataConstraint(const ConstraintProto& ct, Model* m) {
+void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m) {
   auto* mapping = m->GetOrCreate<CpModelMapping>();
   const std::vector<IntegerVariable> vars =
-      mapping->Integers(ct.automata().vars());
+      mapping->Integers(ct.automaton().vars());
 
-  const int num_transitions = ct.automata().transition_tail_size();
+  const int num_transitions = ct.automaton().transition_tail_size();
   std::vector<std::vector<int64>> transitions;
   transitions.reserve(num_transitions);
   for (int i = 0; i < num_transitions; ++i) {
-    transitions.push_back({ct.automata().transition_tail(i),
-                           ct.automata().transition_label(i),
-                           ct.automata().transition_head(i)});
+    transitions.push_back({ct.automaton().transition_tail(i),
+                           ct.automaton().transition_label(i),
+                           ct.automaton().transition_head(i)});
   }
 
-  const int64 starting_state = ct.automata().starting_state();
+  const int64 starting_state = ct.automaton().starting_state();
   const std::vector<int64> final_states =
-      ValuesFromProto(ct.automata().final_states());
+      ValuesFromProto(ct.automaton().final_states());
   m->Add(TransitionConstraint(vars, transitions, starting_state, final_states));
 }
 
@@ -1269,8 +1269,8 @@ bool LoadConstraint(const ConstraintProto& ct, Model* m) {
     case ConstraintProto::ConstraintProto::kTable:
       LoadTableConstraint(ct, m);
       return true;
-    case ConstraintProto::ConstraintProto::kAutomata:
-      LoadAutomataConstraint(ct, m);
+    case ConstraintProto::ConstraintProto::kAutomaton:
+      LoadAutomatonConstraint(ct, m);
       return true;
     case ConstraintProto::ConstraintProto::kCircuit:
       LoadCircuitConstraint(ct, m);
diff --git a/ortools/sat/cp_model_loader.h b/ortools/sat/cp_model_loader.h
index 0b44d85152..d6fd570022 100644
--- a/ortools/sat/cp_model_loader.h
+++ b/ortools/sat/cp_model_loader.h
@@ -190,7 +190,7 @@ void LoadElementConstraintBounds(const ConstraintProto& ct, Model* m);
 void LoadElementConstraintAC(const ConstraintProto& ct, Model* m);
 void LoadElementConstraint(const ConstraintProto& ct, Model* m);
 void LoadTableConstraint(const ConstraintProto& ct, Model* m);
-void LoadAutomataConstraint(const ConstraintProto& ct, Model* m);
+void LoadAutomatonConstraint(const ConstraintProto& ct, Model* m);
 void LoadCircuitConstraint(const ConstraintProto& ct, Model* m);
 void LoadRoutesConstraint(const ConstraintProto& ct, Model* m);
 void LoadCircuitCoveringConstraint(const ConstraintProto& ct, Model* m);
diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc
index 8882900ad5..445c31e23b 100644
--- a/ortools/sat/cp_model_search.cc
+++ b/ortools/sat/cp_model_search.cc
@@ -297,12 +297,18 @@ SatParameters DiversifySearchParameters(const SatParameters& params,
         *name = "fixed";
         return new_params;
       }
+    } else {
+      // TODO(user): Disable lp_br if linear part is small or empty.
+      if (--index == 0) {
+        new_params.set_search_branching(SatParameters::LP_SEARCH);
+        *name = "lp_br";
+        return new_params;
+      }
     }
 
-    // TODO(user): Disable lp_br if linear part is small or empty.
     if (--index == 0) {
       new_params.set_search_branching(SatParameters::PSEUDO_COST_SEARCH);
-      *name = "lp_br";
+      *name = "pseudo_cost";
       return new_params;
     }
 
diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc
index 87e99cf9a0..94d181c074 100644
--- a/ortools/sat/cp_model_solver.cc
+++ b/ortools/sat/cp_model_solver.cc
@@ -154,8 +154,8 @@ class FullEncodingFixedPointComputer {
         return PropagateElement(ct);
       case ConstraintProto::ConstraintProto::kTable:
         return PropagateTable(ct);
-      case ConstraintProto::ConstraintProto::kAutomata:
-        return PropagateAutomata(ct);
+      case ConstraintProto::ConstraintProto::kAutomaton:
+        return PropagateAutomaton(ct);
       case ConstraintProto::ConstraintProto::kInverse:
         return PropagateInverse(ct);
       case ConstraintProto::ConstraintProto::kLinear:
@@ -209,7 +209,7 @@ class FullEncodingFixedPointComputer {
 
   bool PropagateElement(const ConstraintProto* ct);
   bool PropagateTable(const ConstraintProto* ct);
-  bool PropagateAutomata(const ConstraintProto* ct);
+  bool PropagateAutomaton(const ConstraintProto* ct);
   bool PropagateInverse(const ConstraintProto* ct);
   bool PropagateLinear(const ConstraintProto* ct);
 
@@ -268,9 +268,9 @@ bool FullEncodingFixedPointComputer::PropagateTable(const ConstraintProto* ct) {
   return true;
 }
 
-bool FullEncodingFixedPointComputer::PropagateAutomata(
+bool FullEncodingFixedPointComputer::PropagateAutomaton(
     const ConstraintProto* ct) {
-  for (const int variable : ct->automata().vars()) {
+  for (const int variable : ct->automaton().vars()) {
     FullyEncode(variable);
   }
   return true;
diff --git a/ortools/sat/cp_model_utils.cc b/ortools/sat/cp_model_utils.cc
index a28340028e..51f4015ab4 100644
--- a/ortools/sat/cp_model_utils.cc
+++ b/ortools/sat/cp_model_utils.cc
@@ -93,8 +93,8 @@ void AddReferencesUsedByConstraint(const ConstraintProto& ct,
     case ConstraintProto::ConstraintCase::kTable:
       AddIndices(ct.table().vars(), &output->variables);
       break;
-    case ConstraintProto::ConstraintCase::kAutomata:
-      AddIndices(ct.automata().vars(), &output->variables);
+    case ConstraintProto::ConstraintCase::kAutomaton:
+      AddIndices(ct.automaton().vars(), &output->variables);
       break;
     case ConstraintProto::ConstraintCase::kInterval:
       output->variables.insert(ct.interval().start());
@@ -177,7 +177,7 @@ void ApplyToAllLiteralIndices(const std::function<void(int*)>& f,
       break;
     case ConstraintProto::ConstraintCase::kTable:
       break;
-    case ConstraintProto::ConstraintCase::kAutomata:
+    case ConstraintProto::ConstraintCase::kAutomaton:
       break;
     case ConstraintProto::ConstraintCase::kInterval:
       break;
@@ -251,8 +251,8 @@ void ApplyToAllVariableIndices(const std::function<void(int*)>& f,
     case ConstraintProto::ConstraintCase::kTable:
       APPLY_TO_REPEATED_FIELD(table, vars);
       break;
-    case ConstraintProto::ConstraintCase::kAutomata:
-      APPLY_TO_REPEATED_FIELD(automata, vars);
+    case ConstraintProto::ConstraintCase::kAutomaton:
+      APPLY_TO_REPEATED_FIELD(automaton, vars);
       break;
     case ConstraintProto::ConstraintCase::kInterval:
       APPLY_TO_SINGULAR_FIELD(interval, start);
@@ -311,7 +311,7 @@ void ApplyToAllIntervalIndices(const std::function<void(int*)>& f,
       break;
     case ConstraintProto::ConstraintCase::kTable:
       break;
-    case ConstraintProto::ConstraintCase::kAutomata:
+    case ConstraintProto::ConstraintCase::kAutomaton:
       break;
     case ConstraintProto::ConstraintCase::kInterval:
       break;
@@ -372,8 +372,8 @@ std::string ConstraintCaseName(
       return "kReservoir";
     case ConstraintProto::ConstraintCase::kTable:
       return "kTable";
-    case ConstraintProto::ConstraintCase::kAutomata:
-      return "kAutomata";
+    case ConstraintProto::ConstraintCase::kAutomaton:
+      return "kAutomaton";
     case ConstraintProto::ConstraintCase::kInterval:
       return "kInterval";
     case ConstraintProto::ConstraintCase::kNoOverlap:
diff --git a/ortools/sat/csharp/CpModel.cs b/ortools/sat/csharp/CpModel.cs
index 8e4ffdcb40..c0f307c297 100644
--- a/ortools/sat/csharp/CpModel.cs
+++ b/ortools/sat/csharp/CpModel.cs
@@ -402,12 +402,12 @@ public class CpModel
     return ct;
   }
 
-  public Constraint AddAutomata(IEnumerable<IntVar> vars,
+  public Constraint AddAutomaton(IEnumerable<IntVar> vars,
                                 long starting_state,
                                 long[,] transitions,
                                 IEnumerable<long> final_states) {
     Constraint ct = new Constraint(model_);
-    AutomataConstraintProto aut = new AutomataConstraintProto();
+    AutomatonConstraintProto aut = new AutomatonConstraintProto();
     foreach (IntVar var in vars)
     {
       aut.Vars.Add(var.Index);
@@ -424,17 +424,17 @@ public class CpModel
       aut.TransitionHead.Add(transitions[i, 2]);
     }
 
-    ct.Proto.Automata = aut;
+    ct.Proto.Automaton = aut;
     return ct;
   }
 
-  public Constraint AddAutomata(
+  public Constraint AddAutomaton(
       IEnumerable<IntVar> vars,
       long starting_state,
       IEnumerable<Tuple<long, long, long>> transitions,
       IEnumerable<long> final_states) {
     Constraint ct = new Constraint(model_);
-    AutomataConstraintProto aut = new AutomataConstraintProto();
+    AutomatonConstraintProto aut = new AutomatonConstraintProto();
     foreach (IntVar var in vars)
     {
       aut.Vars.Add(var.Index);
@@ -452,7 +452,7 @@ public class CpModel
       aut.TransitionTail.Add(transition.Item3);
     }
 
-    ct.Proto.Automata = aut;
+    ct.Proto.Automaton = aut;
     return ct;
   }
 
diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc
index 68377073e7..6623fac0fe 100644
--- a/ortools/sat/integer.cc
+++ b/ortools/sat/integer.cc
@@ -353,6 +353,9 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal,
     return;
   }
 
+  const IntegerLiteral ge = IntegerLiteral::GreaterOrEqual(var, value);
+  const IntegerLiteral le = IntegerLiteral::LowerOrEqual(var, value);
+
   // Special case for the first and last value.
   if (value == domain.Min()) {
     // Note that this will recursively call AssociateToIntegerEqualValue() but
@@ -360,24 +363,26 @@ void IntegerEncoder::AssociateToIntegerEqualValue(Literal literal,
     // stop there. When a domain has just 2 values, this allows to call just
     // once AssociateToIntegerEqualValue() and also associate the other value to
     // the negation of the given literal.
-    AssociateToIntegerLiteral(literal,
-                              IntegerLiteral::LowerOrEqual(var, value));
+    AssociateToIntegerLiteral(literal, le);
     return;
   }
   if (value == domain.Max()) {
-    AssociateToIntegerLiteral(literal,
-                              IntegerLiteral::GreaterOrEqual(var, value));
+    AssociateToIntegerLiteral(literal, ge);
     return;
   }
 
   // (var == value)  <=>  (var >= value) and (var <= value).
-  const Literal a(
-      GetOrCreateAssociatedLiteral(IntegerLiteral::GreaterOrEqual(var, value)));
-  const Literal b(
-      GetOrCreateAssociatedLiteral(IntegerLiteral::LowerOrEqual(var, value)));
+  const Literal a(GetOrCreateAssociatedLiteral(ge));
+  const Literal b(GetOrCreateAssociatedLiteral(le));
   sat_solver_->AddBinaryClause(a, literal.Negated());
   sat_solver_->AddBinaryClause(b, literal.Negated());
   sat_solver_->AddProblemClause({a.Negated(), b.Negated(), literal});
+
+  // Update reverse encoding.
+  const int new_size = 1 + literal.Index().value();
+  if (new_size > reverse_encoding_.size()) reverse_encoding_.resize(new_size);
+  reverse_encoding_[literal.Index()].push_back(le);
+  reverse_encoding_[literal.Index()].push_back(ge);
 }
 
 // TODO(user): The hard constraints we add between associated literals seems to
diff --git a/ortools/sat/pseudo_costs.cc b/ortools/sat/pseudo_costs.cc
index 621d255014..1b0b9b68de 100644
--- a/ortools/sat/pseudo_costs.cc
+++ b/ortools/sat/pseudo_costs.cc
@@ -126,7 +126,7 @@ std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
   if (decision == kNoLiteralIndex) return bound_changes;
   auto* encoder = model->GetOrCreate<IntegerEncoder>();
   auto* integer_trail = model->GetOrCreate<IntegerTrail>();
-  // TODO(user): Support equality decisions.
+  // NOTE: We ignore negation of equality decisions.
   for (const IntegerLiteral l :
        encoder->GetIntegerLiterals(Literal(decision))) {
     if (l.var == kNoIntegerVariable) continue;
@@ -134,7 +134,7 @@ std::vector<PseudoCosts::VariableBoundChange> GetBoundChanges(
     PseudoCosts::VariableBoundChange var_bound_change;
     var_bound_change.var = l.var;
     const IntegerValue current_lb = integer_trail->LowerBound(l.var);
-    var_bound_change.lower_bound_change = Subtract(l.bound, current_lb);    
+    var_bound_change.lower_bound_change = Subtract(l.bound, current_lb);
     bound_changes.push_back(var_bound_change);
   }
 
diff --git a/ortools/sat/python/cp_model.py b/ortools/sat/python/cp_model.py
index a31aa2466d..a989314222 100644
--- a/ortools/sat/python/cp_model.py
+++ b/ortools/sat/python/cp_model.py
@@ -764,7 +764,7 @@ class CpModel(object):
     and 'transition' is the label of an arc from 'head' to 'tail',
     corresponding to the value of one variable in the list of variables.
 
-    This automata will be unrolled into a flow with n + 1 phases. Each phase
+    This automaton will be unrolled into a flow with n + 1 phases. Each phase
     contains the possible states of the automaton. The first state contains the
     initial state. The last phase contains the final states.
 
@@ -782,10 +782,10 @@ class CpModel(object):
 
     Args:
       transition_variables: A non empty list of variables whose values
-        correspond to the labels of the arcs traversed by the automata.
-      starting_state: The initial state of the automata.
+        correspond to the labels of the arcs traversed by the automaton.
+      starting_state: The initial state of the automaton.
       final_states: A non empty list of admissible final states.
-      transition_triples: A list of transition for the automata, in the
+      transition_triples: A list of transition for the automaton, in the
         following format (current_state, variable_value, next_state).
 
     Returns:
@@ -798,23 +798,23 @@ class CpModel(object):
 
         if not transition_variables:
             raise ValueError(
-                'AddAutomata expects a non empty transition_variables '
+                'AddAutomaton expects a non empty transition_variables '
                 'array')
         if not final_states:
-            raise ValueError('AddAutomata expects some final states')
+            raise ValueError('AddAutomaton expects some final states')
 
         if not transition_triples:
-            raise ValueError('AddAutomata expects some transtion triples')
+            raise ValueError('AddAutomaton expects some transtion triples')
 
         ct = Constraint(self.__model.constraints)
         model_ct = self.__model.constraints[ct.Index()]
-        model_ct.automata.vars.extend(
+        model_ct.automaton.vars.extend(
             [self.GetOrMakeIndex(x) for x in transition_variables])
         cp_model_helper.AssertIsInt64(starting_state)
-        model_ct.automata.starting_state = starting_state
+        model_ct.automaton.starting_state = starting_state
         for v in final_states:
             cp_model_helper.AssertIsInt64(v)
-            model_ct.automata.final_states.append(v)
+            model_ct.automaton.final_states.append(v)
         for t in transition_triples:
             if len(t) != 3:
                 raise TypeError('Tuple ' + str(t) +
@@ -822,9 +822,9 @@ class CpModel(object):
             cp_model_helper.AssertIsInt64(t[0])
             cp_model_helper.AssertIsInt64(t[1])
             cp_model_helper.AssertIsInt64(t[2])
-            model_ct.automata.transition_tail.append(t[0])
-            model_ct.automata.transition_label.append(t[1])
-            model_ct.automata.transition_head.append(t[2])
+            model_ct.automaton.transition_tail.append(t[0])
+            model_ct.automaton.transition_label.append(t[1])
+            model_ct.automaton.transition_head.append(t[2])
         return ct
 
     def AddInverse(self, variables, inverse_variables):
@@ -1558,7 +1558,7 @@ class ObjectiveSolutionPrinter(CpSolverSolutionCallback):
         best_bound = self.BestObjectiveBound()
         obj_lb = min(objective, best_bound)
         obj_ub = max(objective, best_bound)
-        print('Solution %i, time = %.2f s, objective = [%i, %i]' %
-              (self.__solution_count, current_time - self.__start_time,
-               obj_lb, obj_ub))
+        print('Solution %i, time = %f s, objective = [%i, %i]' %
+              (self.__solution_count, current_time - self.__start_time, obj_lb,
+               obj_ub))
         self.__solution_count += 1
diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc
index 2aa05b58e6..9fb104330d 100644
--- a/ortools/sat/table.cc
+++ b/ortools/sat/table.cc
@@ -393,7 +393,7 @@ std::function<void(Model*)> LiteralTableConstraint(
 
 std::function<void(Model*)> TransitionConstraint(
     const std::vector<IntegerVariable>& vars,
-    const std::vector<std::vector<int64>>& automata, int64 initial_state,
+    const std::vector<std::vector<int64>>& automaton, int64 initial_state,
     const std::vector<int64>& final_states) {
   return [=](Model* model) {
     IntegerTrail* integer_trail = model->GetOrCreate<IntegerTrail>();
@@ -403,7 +403,7 @@ std::function<void(Model*)> TransitionConstraint(
     // Test precondition.
     {
       std::set<std::pair<int64, int64>> unique_transition_checker;
-      for (const std::vector<int64>& transition : automata) {
+      for (const std::vector<int64>& transition : automaton) {
         CHECK_EQ(transition.size(), 3);
         const std::pair<int64, int64> p{transition[0], transition[1]};
         CHECK(!gtl::ContainsKey(unique_transition_checker, p))
@@ -417,7 +417,7 @@ std::function<void(Model*)> TransitionConstraint(
     std::vector<absl::flat_hash_set<int64>> possible_values(n);
     for (int time = 0; time < n; ++time) {
       const auto domain = integer_trail->InitialVariableDomain(vars[time]);
-      for (const std::vector<int64>& transition : automata) {
+      for (const std::vector<int64>& transition : automaton) {
         // TODO(user): quadratic algo, improve!
         if (domain.Contains(transition[1])) {
           possible_values[time].insert(transition[1]);
@@ -435,7 +435,7 @@ std::function<void(Model*)> TransitionConstraint(
     // TODO(user): filter using the domain of vars[time] that may not contain
     // all the possible transitions.
     for (int time = 0; time + 1 < n; ++time) {
-      for (const std::vector<int64>& transition : automata) {
+      for (const std::vector<int64>& transition : automaton) {
         if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
         if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
         reachable_states[time + 1].insert(transition[2]);
@@ -445,7 +445,7 @@ std::function<void(Model*)> TransitionConstraint(
     // Backward.
     for (int time = n - 1; time > 0; --time) {
       std::set<int64> new_set;
-      for (const std::vector<int64>& transition : automata) {
+      for (const std::vector<int64>& transition : automaton) {
         if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
         if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
         if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))
@@ -455,7 +455,7 @@ std::function<void(Model*)> TransitionConstraint(
       reachable_states[time].swap(new_set);
     }
 
-    // We will model at each time step the current automata state using Boolean
+    // We will model at each time step the current automaton state using Boolean
     // variables. We will have n+1 time step. At time zero, we start in the
     // initial state, and at time n we should be in one of the final states. We
     // don't need to create Booleans at at time when there is just one possible
@@ -465,13 +465,13 @@ std::function<void(Model*)> TransitionConstraint(
     absl::flat_hash_map<IntegerValue, Literal> out_encoding;
     for (int time = 0; time < n; ++time) {
       // All these vector have the same size. We will use them to enforce a
-      // local table constraint representing one step of the automata at the
+      // local table constraint representing one step of the automaton at the
       // given time.
       std::vector<Literal> tuple_literals;
       std::vector<IntegerValue> in_states;
       std::vector<IntegerValue> transition_values;
       std::vector<IntegerValue> out_states;
-      for (const std::vector<int64>& transition : automata) {
+      for (const std::vector<int64>& transition : automaton) {
         if (!gtl::ContainsKey(reachable_states[time], transition[0])) continue;
         if (!gtl::ContainsKey(possible_values[time], transition[1])) continue;
         if (!gtl::ContainsKey(reachable_states[time + 1], transition[2]))
diff --git a/ortools/sat/table.h b/ortools/sat/table.h
index cce9f1748b..5aa943a70b 100644
--- a/ortools/sat/table.h
+++ b/ortools/sat/table.h
@@ -57,10 +57,10 @@ std::function<void(Model*)> LiteralTableConstraint(
 void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
                     std::vector<std::vector<int64>>* tuples);
 
-// Given an automata defined by a set of 3-tuples:
+// Given an automaton defined by a set of 3-tuples:
 //     (state, transition_with_value_as_label, next_state)
 // this accepts the sequences of vars.size() variables that are recognized by
-// this automata. That is:
+// this automaton. That is:
 //   - We start from the initial state.
 //   - For each variable, we move along the transition labeled by this variable
 //     value. Moreover, the variable must take a value that correspond to a
@@ -71,7 +71,7 @@ void CompressTuples(const std::vector<int64>& domain_sizes, int64 any_value,
 // See the test for some examples.
 std::function<void(Model*)> TransitionConstraint(
     const std::vector<IntegerVariable>& vars,
-    const std::vector<std::vector<int64>>& automata, int64 initial_state,
+    const std::vector<std::vector<int64>>& automaton, int64 initial_state,
     const std::vector<int64>& final_states);
 
 }  // namespace sat