diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 980592f25..f9c108b92 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -1697,7 +1697,7 @@ void parser_example3()
     LOG_MSG("parser_example3");
 
     cfg = Z3_mk_config();
-    /* See quantifer_example1 */
+    /* See quantifier_example1 */
     Z3_set_param_value(cfg, "model", "true");
     ctx = mk_context_custom(cfg, error_handler);
     Z3_del_config(cfg);
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs
index f3a8f9f2c..4f8cdc759 100644
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs
+++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs
@@ -33,14 +33,14 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
 
         #region Solver construction and destruction
 
-        /// <summary>Constructor that initializes the base clases</summary>
+        /// <summary>Constructor that initializes the base classes</summary>
         public Z3MILPSolver() : base(null) 
         {
             _result = LinearResult.Feasible;
             _solver = new Z3BaseSolver(this);
         }
 
-        /// <summary>Constructor that initializes the base clases</summary>
+        /// <summary>Constructor that initializes the base classes</summary>
         public Z3MILPSolver(ISolverEnvironment context) : this() { }
 
         /// <summary>
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs
index 530df3394..de91c7b6e 100644
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs
+++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs
@@ -29,13 +29,13 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
         private NonlinearResult _result;
         private Z3BaseSolver _solver;
 
-        /// <summary>Constructor that initializes the base clases</summary>
+        /// <summary>Constructor that initializes the base classes</summary>
         public Z3TermSolver() : base(null) 
         {
             _solver = new Z3BaseSolver(this);
         }
 
-        /// <summary>Constructor that initializes the base clases</summary>
+        /// <summary>Constructor that initializes the base classes</summary>
         public Z3TermSolver(ISolverEnvironment context) : this() { }
 
         /// <summary>
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index f3d61c1cf..5ee7fcb99 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4094,7 +4094,7 @@ extern "C" {
        The remaining fields are left unchanged. It is the record
        equivalent of an array store (see \sa Z3_mk_store).
        If the datatype has more than one constructor, then the update function
-       behaves as identity if there is a miss-match between the accessor and
+       behaves as identity if there is a mismatch between the accessor and
        constructor. For example ((_ update-field car) nil 1) is nil,
        while ((_ update-field car) (cons 2 nil) 1) is (cons 1 nil).
 
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index f4a538abd..01b06518e 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -147,7 +147,7 @@ namespace datalog {
         for (unsigned i = 0; i < n; ++i) {
             parameter const& p = r->get_parameter(i);
             if (!p.is_ast() || !is_sort(p.get_ast())) {
-                m_manager->raise_exception("exptected sort parameter");
+                m_manager->raise_exception("expected sort parameter");
                 return false;
             }
             sorts.push_back(to_sort(p.get_ast()));
@@ -185,7 +185,7 @@ namespace datalog {
                            verbose_stream() << "Domain: " << mk_pp(domain[0], m) << "\n" <<
                            mk_pp(sorts[i], m) << "\n" <<
                            mk_pp(domain[i+1], m) << "\n";);
-                m_manager->raise_exception("sort miss-match for relational access");
+                m_manager->raise_exception("sort mismatch for relational access");
                 return nullptr;
             }
         }
@@ -252,7 +252,7 @@ namespace datalog {
     func_decl * dl_decl_plugin::mk_unionw(decl_kind k, sort* s1, sort* s2) {
         ast_manager& m = *m_manager;
         if (s1 != s2) {
-            m_manager->raise_exception("sort miss-match for arguments to union");
+            m_manager->raise_exception("sort mismatch for arguments to union");
             return nullptr;
         }
         if (!is_rel_sort(s1)) {                
@@ -298,7 +298,7 @@ namespace datalog {
                     return nullptr;
                 }
                 if (sorts[idx] != m.get_sort(e)) {
-                    m_manager->raise_exception("sort miss-match in filter");
+                    m_manager->raise_exception("sort mismatch in filter");
                     return nullptr;
                 }
                 break;
@@ -391,7 +391,7 @@ namespace datalog {
                 return nullptr;
             }
             if (sorts1[i1] != sorts2[i2]) {
-                m_manager->raise_exception("sort miss-match in join");
+                m_manager->raise_exception("sort mismatch in join");
                 return nullptr;
             }
         }
@@ -435,7 +435,7 @@ namespace datalog {
                 return nullptr;
             }
             if (sorts1[i1] != sorts2[i2]) {
-                m_manager->raise_exception("sort miss-match in join");
+                m_manager->raise_exception("sort mismatch in join");
                 return nullptr;
             }
         }
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 1c9abf78c..e8578f327 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -658,7 +658,7 @@ namespace datalog {
     void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) {
         if (pred->get_arity() != num_args) {
             std::ostringstream out;
-            out << "miss-matched number of arguments passed to " << mk_ismt2_pp(pred, m) << " " << num_args << " passed";
+            out << "mismatched number of arguments passed to " << mk_ismt2_pp(pred, m) << " " << num_args << " passed";
             throw default_exception(out.str());
         }
         table_fact fact;
@@ -1243,7 +1243,7 @@ namespace datalog {
     void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) {
         //
         // replace bound variables in rules by 'var declarations'
-        // First remove quantifers, then replace bound variables
+        // First remove quantifiers, then replace bound variables
         // by fresh constants.
         //
         smt2_pp_environment_dbg env(m);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d48a6410c..fc5fce252 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2665,7 +2665,7 @@ namespace sat {
         for (unsigned i = head; i < sz; i++) {
             literal l  = m_trail[i];
             bool_var v = l.var();
-            TRACE("forget_phase", tout << "forgeting phase of l: " << l << "\n";);
+            TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";);
             m_phase[v] = PHASE_NOT_AVAILABLE;
         }
     }
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7ee6d4a92..3c601f400 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1813,7 +1813,7 @@ namespace smt {
     }
 
     /**
-       \brief Execute next clase split, return false if there are no
+       \brief Execute next case split, return false if there are no
        more case splits to be performed.
     */
     bool context::decide() {
@@ -1858,7 +1858,7 @@ namespace smt {
 
         if (is_quantifier(m_bool_var2expr[var])) {
             // Overriding any decision on how to assign the quantifier.
-            // assigining a quantifier to false is equivalent to make it irrelevant.
+            // assigning a quantifier to false is equivalent to make it irrelevant.
             phase = l_false;
         }
 
@@ -2134,7 +2134,7 @@ namespace smt {
        \brief When a clause is reinitialized (see reinit_clauses) enodes and literals may
        need to be recreated. When an enode is recreated, I want to use the same generation
        number it had before being deleted. Otherwise the generation will be 0, and will affect
-       the loop prevetion heuristics used to control quantifier instantiation.
+       the loop prevention heuristics used to control quantifier instantiation.
        Thus, I cache the generation number of enodes that will be deleted during backtracking
        and recreated by reinit_clauses.
     */
@@ -3872,7 +3872,7 @@ namespace smt {
         for (unsigned i = head; i < sz; i++) {
             literal l  = m_assigned_literals[i];
             bool_var v = l.var();
-            TRACE("forget_phase", tout << "forgeting phase of l: " << l << "\n";);
+            TRACE("forget_phase", tout << "forgetting phase of l: " << l << "\n";);
             m_bdata[v].m_phase_available = false;
         }
     }
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 30ea7b18e..111b9a0c0 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -1703,7 +1703,7 @@ namespace smt {
             friend class quantifier_analyzer;
 
             void checkpoint() {
-                m_mf.checkpoint("quantifer_info");
+                m_mf.checkpoint("quantifier_info");
             }
 
             void insert_qinfo(qinfo * qi) {