7 files changed, 8 insertions, 8 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index c0946c86a..7bfe8d592 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -501,7 +501,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "intial splits on zero for all variables"
+  help       = "initial splits on zero for all variables"
 
 [[option]]
   name       = "nlExtTfTaylorDegree"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 8d71e2f65..740c2e5e6 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -138,7 +138,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , ca                 ()
 
   // even though these are temporaries and technically should be set
-  // before calling, lets intialize them. this will reduces chances of
+  // before calling, lets initialize them. this will reduces chances of
   // non-determinism in portfolio (parallel) solver if variables are
   // being (incorrectly) used without initialization.
   , seen(),  analyze_stack(), analyze_toclear(), add_tmp()
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 748bf12da..c33e2c6b7 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -173,7 +173,7 @@ class FirstOrderModel : public TheoryModel
   std::map<Node, std::map<Node, int> > d_quant_var_id;
   /** process initialize model for term */
   virtual void processInitializeModelForTerm(Node n) = 0;
-  /** process intialize quantifier */
+  /** process initialize quantifier */
   virtual void processInitializeQuantifier(Node q) {}
   /** process initialize */
   virtual void processInitialize(bool ispre) = 0;
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index f094b9490..ce4186eb2 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -77,7 +77,7 @@ class Cegis : public SygusModule
    */
   Node d_base_body;
   //----------------------------------cegis-implementation-specific
-  /** do cegis-implementation-specific intialization for this class */
+  /** do cegis-implementation-specific initialization for this class */
   virtual bool processInitialize(Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& lemmas);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 48fca53f5..858a83bce 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -236,7 +236,7 @@ class CegisUnif : public Cegis
   Node getNextDecisionRequest(unsigned& priority) override;
 
  private:
-  /** do cegis-implementation-specific intialization for this class */
+  /** do cegis-implementation-specific initialization for this class */
   bool processInitialize(Node n,
                          const std::vector<Node>& candidates,
                          std::vector<Node>& lemmas) override;
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 4efc171d3..3f18a65d6 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -65,7 +65,7 @@ class TermRecBuild
   /** get the i^th child of the active term */
   Node getChild(unsigned i);
   /** build the (modified) version of the term
-   * we intialized via the call to init().
+   * we initialized via the call to init().
    */
   Node build(unsigned p = 0);
 
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 0134b3a86..f90c6ebd0 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -50,7 +50,7 @@ namespace quantifiers {
  * For example, say the grammar for f is:
  *   A = 0 | 1 | x | y | A+A | ite( B, A, A )
  *   B = A <= A
- * If we call intialize( tds, f, 5 ), this class will generate 5 random sample
+ * If we call initialize( tds, f, 5 ), this class will generate 5 random sample
  * points for (x,y), say (0,0), (1,1), (0,1), (1,0), (2,2). The return values
  * of successive calls to registerTerm are listed below.
  *   registerTerm( 0 ) -> 0
@@ -281,7 +281,7 @@ class SygusSampler : public LazyTrieEvaluator
   std::map<Node, std::vector<TypeNode> > d_var_sygus_types;
   /** map from constants to sygus types that include them */
   std::map<Node, std::vector<TypeNode> > d_const_sygus_types;
-  /** register sygus type, intializes the above two data structures */
+  /** register sygus type, initializes the above two data structures */
   void registerSygusType(TypeNode tn);
 };