3 files changed, 13 insertions, 13 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 0d2f94f91..e1cdc5ec3 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -131,7 +131,7 @@ bool InferInfo::isFact() const
   return !atom.isConst() && atom.getKind() != kind::OR && d_noExplain.empty();
 }
 
-Node InferInfo::getAntecedant() const
+Node InferInfo::getAntecedent() const
 {
   // d_noExplain is a subset of d_ant
   return utils::mkAnd(d_ant);
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 4c5674d2b..70048b2fa 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -56,7 +56,7 @@ enum class Inference : uint32_t
   //   explain_constant(x, c) => x = c
   // Above, explain_constant(x,c) is a basic explanation of why x must be equal
   // to string constant c, which is computed by taking arguments of
-  // concatentation terms that are entailed to be constants. For example:
+  // concatenation terms that are entailed to be constants. For example:
   //  ( y = "AB" ^ z = "C" ) => y ++ z = "ABC"
   I_CONST_MERGE,
   // initial constant conflict
@@ -355,7 +355,7 @@ class InferenceManager;
  * send a fact, lemma, or conflict that is waiting to be asserted to the
  * equality engine or sent on the output channel.
  *
- * For the sake of proofs, the antecedants in InferInfo have a particular
+ * For the sake of proofs, the antecedents in InferInfo have a particular
  * ordering for many of the core strings rules, which is expected by
  * InferProofCons for constructing proofs of F_CONST, F_UNIFY, N_CONST, etc.
  * which apply to a pair of string terms t and s. At a high level, the ordering
@@ -365,7 +365,7 @@ class InferenceManager;
  * (3) (optionally) a length constraint.
  * For example, say we have:
  *   { x ++ y ++ v1 = z ++ w ++ v2, x = z ++ u, u = "", len(y) = len(w) }
- * We can conclude y = w by the N_UNIFY rule from the left side. The antecedant
+ * We can conclude y = w by the N_UNIFY rule from the left side. The antecedent
  * has the following form:
  * - (prefix up to y/w equal) x = z ++ u, u = "",
  * - (main equality) x ++ y ++ v1 = z ++ w ++ v2,
@@ -387,15 +387,15 @@ class InferInfo : public TheoryInference
   /** The conclusion */
   Node d_conc;
   /**
-   * The antecedant(s) of the inference, interpreted conjunctively. These are
+   * The antecedent(s) of the inference, interpreted conjunctively. These are
    * literals that currently hold in the equality engine.
    */
   std::vector<Node> d_ant;
   /**
-   * The "new literal" antecedant(s) of the inference, interpreted
+   * The "new literal" antecedent(s) of the inference, interpreted
    * conjunctively. These are literals that were needed to show the conclusion
    * but do not currently hold in the equality engine. These should be a subset
-   * of d_ant. In other words, antecedants that are not explained are stored
+   * of d_ant. In other words, antecedents that are not explained are stored
    * in *both* d_ant and d_noExplain.
    */
   std::vector<Node> d_noExplain;
@@ -409,17 +409,17 @@ class InferInfo : public TheoryInference
   bool isTrivial() const;
   /**
    * Does this infer info correspond to a conflict? True if d_conc is false
-   * and it has no new antecedants (d_noExplain).
+   * and it has no new antecedents (d_noExplain).
    */
   bool isConflict() const;
   /**
    * Does this infer info correspond to a "fact". A fact is an inference whose
    * conclusion should be added as an equality or predicate to the equality
-   * engine with no new external antecedants (d_noExplain).
+   * engine with no new external antecedents (d_noExplain).
    */
   bool isFact() const;
-  /** Get antecedant */
-  Node getAntecedant() const;
+  /** Get antecedent */
+  Node getAntecedent() const;
 };
 
 /**
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index e324689f5..b982f24a1 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -329,10 +329,10 @@ bool InferenceManager::processFact(InferInfo& ii)
   {
     facts.push_back(ii.d_conc);
   }
-  Trace("strings-assert") << "(assert (=> " << ii.getAntecedant() << " "
+  Trace("strings-assert") << "(assert (=> " << ii.getAntecedent() << " "
                           << ii.d_conc << ")) ; fact " << ii.d_id << std::endl;
   Trace("strings-lemma") << "Strings::Fact: " << ii.d_conc << " from "
-                         << ii.getAntecedant() << " by " << ii.d_id
+                         << ii.getAntecedent() << " by " << ii.d_id
                          << std::endl;
   std::vector<Node> exp;
   for (const Node& ec : ii.d_ant)