diff --git a/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2 b/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2
index 45ce586f1cc..746767809a4 100644
--- a/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2	
+++ b/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2	
@@ -50,7 +50,7 @@
     )
 )
 
-; Transition funcion
+; Transition function
 (define-fun body ((f_0 Int) (f Int) (i_0 Int) (i_1 Int)(_A (Array Int Int)) (_x Int)) Bool
     (and
         (= f (ite (= _x (select _A i_0)) 1 f_0))
diff --git a/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2 b/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2
index ceb7928757b..a4db5dd98e9 100644
--- a/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2	
+++ b/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2	
@@ -52,7 +52,7 @@
     )
 )
 
-; Transition funcion
+; Transition function
 (define-fun body ((f_0 IntValue) (f IntValue) (i_0 IntValue) (i_1 IntValue)(_A (Array IntValue IntValue)) (_x IntValue)) Bool
     (and
         (= f (ite (= _x (select _A i_0)) #x00000001 f_0))
diff --git a/examples/python/proofreplay.py b/examples/python/proofreplay.py
index c8c9ff47eb4..5c82f43a96c 100644
--- a/examples/python/proofreplay.py
+++ b/examples/python/proofreplay.py
@@ -86,7 +86,7 @@
     # The pair -inst 2 indicates that two quantifier instantiations were not self-validated
     # They were instead validated using a call to SMT solving. A log for an smt invocation
     # is exemplified in the next line.
-    # Note that the pair +inst 6 indicates that 6 quantifier instantations were validated
+    # Note that the pair +inst 6 indicates that 6 quantifier instantiations were validated
     # using a syntactic (cheap) check. Some quantifier instantiations based on quantifier elimination
     # are not simple substitutions and therefore a simple syntactic check does not suffice.
     set_param("solver.proof.check", True)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 2f34b91f69f..37f161a051f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8984,7 +8984,7 @@ def substitute_funs(t, *m):
             m = m1
     if z3_debug():
         _z3_assert(is_expr(t), "Z3 expression expected")
-        _z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, funcion pairs expected.")
+        _z3_assert(all([isinstance(p, tuple) and is_func_decl(p[0]) and is_expr(p[1]) for p in m]), "Z3 invalid substitution, function pairs expected.")
     num = len(m)
     _from = (FuncDecl * num)()
     _to = (Ast * num)()
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 12ab1cbb19d..aa581322485 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -3478,7 +3478,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) {
 // 
 // restrict(d, false) = []
 // 
-// it is already assumed that the restriction takes place witin a branch
+// it is already assumed that the restriction takes place within a branch
 // so the condition is not added explicitly but propagated down in order to eliminate 
 // infeasible cases
 expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond) {
@@ -3717,7 +3717,7 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
         result = re().mk_plus(re().mk_full_char(ele_sort));
     else if (re().is_concat(r, r1, r2))
         // create the resulting concatenation in right-associative form except for the following case
-        // TODO: maintain the followig invariant for A ++ B{m,n} + C
+        // TODO: maintain the following invariant for A ++ B{m,n} + C
         //       concat(concat(A, B{m,n}), C) (if A != () and C != ()) 
         //       concat(B{m,n}, C) (if A == () and C != ()) 
         // where A, B, C are regexes
@@ -3725,11 +3725,11 @@ expr_ref seq_rewriter::mk_regex_concat(expr* r, expr* s) {
         // In other words, do not make A ++ B{m,n} into right-assoc form, but keep B{m,n} at the top 
         // This will help to identify this situation in the merge routine:
         //               concat(concat(A, B{0,m}), C) | concat(concat(A, B{0,n}), C)
-        // simplies to 
+        // simplifies to
         //               concat(concat(A, B{0,max(m,n)}), C)
         // analogously:
         //               concat(concat(A, B{0,m}), C) & concat(concat(A, B{0,n}), C)
-        // simplies to 
+        // simplifies to
         //               concat(concat(A, B{0,min(m,n)}), C)
         result = mk_regex_concat(r1, mk_regex_concat(r2, s));
     else {
@@ -3850,12 +3850,12 @@ bool seq_rewriter::pred_implies(expr* a, expr* b) {
     Utility function to decide if two BDDs (nested if-then-else terms)
     have exactly the same structure and conditions.
 */
-bool seq_rewriter::ite_bdds_compatabile(expr* a, expr* b) {
+bool seq_rewriter::ite_bdds_compatible(expr* a, expr* b) {
     expr* ca = nullptr, *a1 = nullptr, *a2 = nullptr;
     expr* cb = nullptr, *b1 = nullptr, *b2 = nullptr;
     if (m().is_ite(a, ca, a1, a2) && m().is_ite(b, cb, b1, b2)) {
-        return (ca == cb) && ite_bdds_compatabile(a1, b1)
-                          && ite_bdds_compatabile(a2, b2);
+        return (ca == cb) && ite_bdds_compatible(a1, b1)
+                          && ite_bdds_compatible(a2, b2);
     }
     else if (m().is_ite(a) || m().is_ite(b)) {
         return false;
@@ -3915,7 +3915,7 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
         // sophisticated: in an antimirov union of n terms, we really
         // want to check if any pair of them is compatible.
         else if (m().is_ite(a) && m().is_ite(b) &&
-                 !ite_bdds_compatabile(a, b)) {
+                 !ite_bdds_compatible(a, b)) {
             k = _OP_RE_ANTIMIROV_UNION;
         }
         #endif
@@ -4269,7 +4269,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
     }
     else if (re().is_reverse(r, r1)) {
         if (re().is_to_re(r1, r2)) {
-            // First try to exctract hd and tl such that r = hd ++ tl and |tl|=1
+            // First try to extract hd and tl such that r = hd ++ tl and |tl|=1
             expr_ref hd(m()), tl(m());
             if (get_head_tail_reversed(r2, hd, tl)) {
                 // Use mk_der_cond to normalize
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 92a6a17faf6..af4756576ae 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -201,7 +201,7 @@ class seq_rewriter {
     expr_ref mk_der_compl(expr* a);
     expr_ref mk_der_cond(expr* cond, expr* ele, sort* seq_sort);
     expr_ref mk_der_antimirov_union(expr* r1, expr* r2);
-    bool ite_bdds_compatabile(expr* a, expr* b);
+    bool ite_bdds_compatible(expr* a, expr* b);
     /* if r has the form deriv(en..deriv(e1,to_re(s))..) returns 's = [e1..en]' else returns '() in r'*/
     expr_ref is_nullable_symbolic_regex(expr* r, sort* seq_sort);
     #ifdef Z3DEBUG
diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h
index 4b828abf644..4e327f0fa43 100644
--- a/src/ast/rewriter/seq_skolem.h
+++ b/src/ast/rewriter/seq_skolem.h
@@ -8,7 +8,7 @@ Module Name:
 Abstract:
 
     Skolem function support for sequences.
-    Skolem functions are auxiliary funcions useful for axiomatizing sequence
+    Skolem functions are auxiliary functions useful for axiomatizing sequence
     operations.
 
 Author:
diff --git a/src/opt/opt_lns.cpp b/src/opt/opt_lns.cpp
index ba5a071d303..878c4a3ea34 100644
--- a/src/opt/opt_lns.cpp
+++ b/src/opt/opt_lns.cpp
@@ -196,7 +196,7 @@ namespace opt {
     }
 
     unsigned lns::improve_linear(model_ref& mdl) {
-        scoped_bounding _scoped_bouding(*this);
+        scoped_bounding _scoped_bounding(*this);
         unsigned num_improved = 0;
         unsigned max_conflicts = m_max_conflicts;
         while (m.inc()) {
diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 91813c697f2..255c4f8144e 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -674,7 +674,7 @@ namespace mbp {
                     id = mbo.add_var(r, a.is_int(v));
                     tids.insert(v, id);
                 }
-                CTRACE("qe", kv.m_value.is_zero(), tout << mk_pp(v, m) << " has coefficeint 0\n";);
+                CTRACE("qe", kv.m_value.is_zero(), tout << mk_pp(v, m) << " has coefficient 0\n";);
                 if (!kv.m_value.is_zero()) {
                     coeffs.push_back(var(id, kv.m_value));
                 }
diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp
index d46a09284c2..3820af59e12 100644
--- a/src/qe/mbp/mbp_solve_plugin.cpp
+++ b/src/qe/mbp/mbp_solve_plugin.cpp
@@ -248,7 +248,7 @@ namespace mbp {
             return false;
         }
 
-        // returns `true` if a rewritting happened
+        // returns `true` if a rewriting happened
         bool try_int_mul_solve(expr *atom, bool is_pos, expr_ref &res) {
 
             if (!is_pos)
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index 12365b2040e..325f343b467 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -157,8 +157,8 @@ namespace qe {
 
         //
         // Partition variables into buckets.
-        // The var_paritions buckets covering disjoint subsets of
-        // the conjuncts. The remaining variables in vars are non-partioned.
+        // The var_partitions buckets covering disjoint subsets of
+        // the conjuncts. The remaining variables in vars are non-partitioned.
         // 
         bool partition_vars(
             unsigned               num_vars,
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 861c841a939..97f12238d41 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -416,7 +416,7 @@ class mbproj::impl {
             //don't use mbp_qel on some theories where model evaluation is
             //incomplete This is not a limitation of qel. Fix this either by
             //making mbp choices less dependent on the model evaluation methods
-            //or fix theory rewriters to make terms evalution complete
+            //or fix theory rewriters to make terms evaluation complete
             if (m_use_qel && !has_unsupported_th(fmls)) {
                 bool dsub = m_dont_sub;
                 m_dont_sub = !force_elim;
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index b6d1e2f2b0f..2b18d9a3f33 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1830,7 +1830,7 @@ namespace smt {
             // Case) there is a variable old_v in the var-list of n.
             //
             // Remark: This variable was moved to the var-list of n due to a add_eq.
-            SASSERT(th->get_enode(old_v) != n); // this varialbe is not owned by n
+            SASSERT(th->get_enode(old_v) != n); // this variable is not owned by n
             SASSERT(n->get_root()->get_th_var(th_id) != null_theory_var); // the root has also a variable in its var-list.
             n->replace_th_var(v, th_id);
             push_trail(replace_th_var_trail( n, th_id, old_v));
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 4746040ce52..cb3a83a0d7a 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -503,7 +503,7 @@ namespace smt {
         theory_var x_i = r.get_base_var();
         
         SASSERT(is_int(x_i));
-        // The following assertion is wrong. It may be violated in mixed-real-interger problems.
+        // The following assertion is wrong. It may be violated in mixed-real-integer problems.
         // The check is_gomory_cut_target will discard rows where any variable contains infinitesimals.
         // SASSERT(m_value[x_i].is_rational()); // infinitesimals are not used for integer variables
         SASSERT(!m_value[x_i].is_int());     // the base variable is not assigned to an integer value.
diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index da2883938fa..2072474b017 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -11,7 +11,7 @@ Module Name:
 
 Revision History:
 
-    The implementaton is derived from theory_diff_logic.
+    The implementation is derived from theory_diff_logic.
 
 --*/
 #include "smt/theory_utvpi.h"
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index 411b8aa6edb..dce1fe459fe 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -905,10 +905,10 @@ class tseitin_cnf_tactic : public tactic {
 
     void collect_param_descrs(param_descrs & r) override {
         insert_max_memory(r);
-        r.insert("common_patterns", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns", "true");
+        r.insert("common_patterns", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifying commonly used patterns", "true");
         r.insert("distributivity", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas", "true");
         r.insert("distributivity_blowup", CPK_UINT, "maximum overhead for applying distributivity during CNF encoding", "32");
-        r.insert("ite_chaing", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains", "true");                                                       
+        r.insert("ite_chaing", CPK_BOOL, "minimize the number of auxiliary variables during CNF encoding by identifying if-then-else chains", "true");                                                       
         r.insert("ite_extra", CPK_BOOL, "add redundant clauses (that improve unit propagation) when encoding if-then-else formulas", "true");
     }
     
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index b5ea4d6c1dd..4d695e300fc 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -64,7 +64,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
     }
 
     /**
-    * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state
+    * size(), [](), update() and inconsistent() implement the abstract interface of dependent_expr_state
     */
     unsigned qtail() const override { return m_goal->size(); }
 
diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp
index 01370812f75..4d0912fdca7 100644
--- a/src/tactic/fd_solver/smtfd_solver.cpp
+++ b/src/tactic/fd_solver/smtfd_solver.cpp
@@ -433,7 +433,7 @@ namespace smtfd {
         void populate_model(model_ref& mdl, expr_ref_vector const& terms);
 
         /**
-         * \brief check consistency properties that can only be achived using a global analysis of terms
+         * \brief check consistency properties that can only be achieved using a global analysis of terms
          */
         void global_check(expr_ref_vector const& core);
 
diff --git a/src/tactic/goal_proof_converter.h b/src/tactic/goal_proof_converter.h
index a17ff0ea1ea..cfe0d970998 100644
--- a/src/tactic/goal_proof_converter.h
+++ b/src/tactic/goal_proof_converter.h
@@ -37,7 +37,7 @@ class subgoal_proof_converter : public proof_converter {
     }
 
     proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
-        // ignore the proofs from the arguments, instead obtain the proofs fromt he subgoals.
+        // ignore the proofs from the arguments, instead obtain the proofs from the subgoals.
         SASSERT(num_source == 0);
         proof_converter_ref_buffer pc_buffer;          
         for (goal_ref g : m_goals) {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.h b/src/tactic/ufbv/quasi_macros_tactic.h
index faa939954fb..ec2a455276e 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.h
+++ b/src/tactic/ufbv/quasi_macros_tactic.h
@@ -18,7 +18,7 @@ Tactic Documentation
 ## Tactic quasi-macro-finder
 
 ### Short Description
-dentifies and applies quasi-macros.
+Identifies and applies quasi-macros.
 
 ### Long Description
 
diff --git a/src/test/lp/smt_reader.h b/src/test/lp/smt_reader.h
index 7a0ea5ff989..0e638399fb8 100644
--- a/src/test/lp/smt_reader.h
+++ b/src/test/lp/smt_reader.h
@@ -343,7 +343,7 @@ namespace lp {
             solver->add_constraint(&c);
         }
 
-        void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) {
+        void create_equality_constraint_for_var(column* col, bound * b, lar_solver *solver) {
             lar_constraint c(EQ, b->m_fixed_value);
             var_index i = solver->add_var(col->m_name);
             c.add_variable_to_constraint(i, numeric_traits<T>::one());
@@ -366,7 +366,7 @@ namespace lp {
                     create_upper_constraint_for_var(col, b, solver);
                 }
                 if (b->m_value_is_fixed) {
-                    create_equality_contraint_for_var(col, b, solver);
+                    create_equality_constraint_for_var(col, b, solver);
                 }
             }
         }
diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp
index 694f13e9650..2c76b3a6636 100644
--- a/src/test/mpz.cpp
+++ b/src/test/mpz.cpp
@@ -322,7 +322,7 @@ void tst_scoped() {
 #define NUM_PRIMES 168
 unsigned g_primes[NUM_PRIMES] = { 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 101, 103, 107, 109, 113, 127, 131, 137, 139, 149, 151, 157, 163, 167, 173, 179, 181, 191, 193, 197, 199, 211, 223, 227, 229, 233, 239, 241, 251, 257, 263, 269, 271, 277, 281, 283, 293, 307, 311, 313, 317, 331, 337, 347, 349, 353, 359, 367, 373, 379, 383, 389, 397, 401, 409, 419, 421, 431, 433, 439, 443, 449, 457, 461, 463, 467, 479, 487, 491, 499, 503, 509, 521, 523, 541, 547, 557, 563, 569, 571, 577, 587, 593, 599, 601, 607, 613, 617, 619, 631, 641, 643, 647, 653, 659, 661, 673, 677, 683, 691, 701, 709, 719, 727, 733, 739, 743, 751, 757, 761, 769, 773, 787, 797, 809, 811, 821, 823, 827, 829, 839, 853, 857, 859, 863, 877, 881, 883, 887, 907, 911, 919, 929, 937, 941, 947, 953, 967, 971, 977, 983, 991, 997 };
 
-// Return a big number by multipling powers of the first NUM_PRIMES.
+// Return a big number by multiplying powers of the first NUM_PRIMES.
 // - ratio:  rand() % ratio == 0 is used to decide whether a specific prime will be included or not.
 // - max_pw: if condition above is satisfied, then we use (rand() % max_pw) + 1 as the power.
 void mk_big_num(unsynch_mpz_manager & m, unsigned ratio, unsigned max_pw, mpz & r) {