diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 05018df10..0e2cab37e 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -570,7 +570,7 @@ void tactic_example3() {
       - The choice combinator t | s first applies t to the given goal, if it fails then returns the result of s applied to the given goal.      
       - repeat(t) Keep applying the given tactic until no subgoal is modified by it.
       - repeat(t, n) Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than n.
-      - try_for(t, ms) Apply tactic t to the input goal, if it does not return in ms millisenconds, it fails.
+      - try_for(t, ms) Apply tactic t to the input goal, if it does not return in ms milliseconds, it fails.
       - with(t, params) Apply the given tactic using the given parameters.      
     */
     std::cout << "tactic example 3\n";
diff --git a/examples/python/hamiltonian/hamiltonian.py b/examples/python/hamiltonian/hamiltonian.py
index 350205a65..6906ee477 100644
--- a/examples/python/hamiltonian/hamiltonian.py
+++ b/examples/python/hamiltonian/hamiltonian.py
@@ -64,7 +64,7 @@ def examples():
     print(sdodec.model())
     # =======================================================
     # See http://en.wikipedia.org/wiki/Hamiltonian_path for the Herschel graph
-    # being the smallest possible polyhdral graph that does not have a Hamiltonian
+    # being the smallest possible polyhedral graph that does not have a Hamiltonian
     # cycle.
     #
     grherschel = { 0: [1, 9, 10, 7],
diff --git a/examples/python/mus/mss.py b/examples/python/mus/mss.py
index c7b44c8a4..9156c3095 100644
--- a/examples/python/mus/mss.py
+++ b/examples/python/mus/mss.py
@@ -118,11 +118,11 @@ class MSSSolver:
 
    # Given a current satisfiable state
    # Extract an MSS, and ensure that currently 
-   # encoutered cores are avoided in next iterations
+   # encountered cores are avoided in next iterations
    # by weakening the set of literals that are
    # examined in next iterations.
    # Strengthen the solver state by enforcing that
-   # an element from the MCS is encoutered.
+   # an element from the MCS is encountered.
 
    def grow(self):
        self.mss = []
diff --git a/examples/python/rc2.py b/examples/python/rc2.py
index 1a07b3bf2..c4e811eb1 100644
--- a/examples/python/rc2.py
+++ b/examples/python/rc2.py
@@ -74,7 +74,7 @@ class RC2:
     def get_cost(self):
         return sum(self.Ws0[c] for c in self.Ws0 if not tt(self.solver, c))
 
-    # Retrieve independendent cores from Ws
+    # Retrieve independent cores from Ws
     def get_cores(self, Ws):
         cores = []
         while unsat == self.check(Ws):            
diff --git a/examples/python/socrates.py b/examples/python/socrates.py
index 8d44b41ea..bd7c1f7c4 100644
--- a/examples/python/socrates.py
+++ b/examples/python/socrates.py
@@ -26,7 +26,7 @@ axioms = [ForAll([x], Implies(Human(x), Mortal(x))),
 s = Solver()
 s.add(axioms)
 
-print(s.check()) # prints sat so axioms are coherents
+print(s.check()) # prints sat so axioms are coherent
 
 # classical refutation
 s.add(Not(Mortal(socrates)))
diff --git a/examples/python/tutorial/html/advanced-examples.htm b/examples/python/tutorial/html/advanced-examples.htm
index e578aade8..d154461b2 100644
--- a/examples/python/tutorial/html/advanced-examples.htm
+++ b/examples/python/tutorial/html/advanced-examples.htm
@@ -505,7 +505,7 @@ and <tt>y</tt> were used to create quantified formulas.
 This is a "trick" for simplifying the construction of quantified
 formulas in Z3Py. Internally, these constants are replaced by
 bounded variables. The next example demonstrates that. The method
-<tt>body()</tt> retrives the quantified expression.
+<tt>body()</tt> retrieves the quantified expression.
 In the resultant formula the bounded variables are free.
 The function <tt>Var(index, sort)</tt> creates a bounded/free variable
 with the given index and sort.
@@ -603,7 +603,7 @@ Z3 fails to show that the formula is unsatisfiable.
 </body></html></example>
 
 <p>When the more permissive pattern <tt>g(x)</tt> is used. Z3 proves the formula
-to be unsatisfiable. More restrive patterns minimize the number of
+to be unsatisfiable. More restrictive patterns minimize the number of
 instantiations (and potentially improve performance), but they may
 also make Z3 "less complete".
 </p>
diff --git a/examples/python/tutorial/html/strategies-examples.htm b/examples/python/tutorial/html/strategies-examples.htm
index 0d5e6424b..791325efb 100644
--- a/examples/python/tutorial/html/strategies-examples.htm
+++ b/examples/python/tutorial/html/strategies-examples.htm
@@ -118,7 +118,7 @@ if it fails then returns the result of <tt>s</tt> applied to the given goal.
 the number of iterations is greater than <tt>n</tt>.
 </li>
 <li> <tt>TryFor(t, ms)</tt> Apply tactic <tt>t</tt> to the input goal, if it does not return in
-<tt>ms</tt> millisenconds, it fails.
+<tt>ms</tt> milliseconds, it fails.
 </li>
 <li> <tt>With(t, params)</tt> Apply the given tactic using the given parameters.
 </li>
diff --git a/examples/python/tutorial/jupyter/advanced.ipynb b/examples/python/tutorial/jupyter/advanced.ipynb
index 5dba6f09e..01ab0ae67 100644
--- a/examples/python/tutorial/jupyter/advanced.ipynb
+++ b/examples/python/tutorial/jupyter/advanced.ipynb
@@ -527,7 +527,7 @@
    "source": [
     "Nevertheless, Z3 is often able to handle formulas involving quantifiers. It uses several approaches to handle quantifiers. The most prolific approach is using pattern-based quantifier instantiation. This approach allows instantiating quantified formulas with ground terms that appear in the current search context based on pattern annotations on quantifiers. Z3 also contains a model-based quantifier instantiation component that uses a model construction to find good terms to instantiate quantifiers with; and Z3 also handles many decidable fragments.\n",
     "\n",
-    "Note that in the previous example the constants x and y were used to create quantified formulas. This is a \"trick\" for simplifying the construction of quantified formulas in Z3Py. Internally, these constants are replaced by bounded variables. The next example demonstrates that. The method body() retrives the quantified expression. In the resultant formula the bounded variables are free. The function Var(index, sort) creates a bounded/free variable with the given index and sort."
+    "Note that in the previous example the constants x and y were used to create quantified formulas. This is a \"trick\" for simplifying the construction of quantified formulas in Z3Py. Internally, these constants are replaced by bounded variables. The next example demonstrates that. The method body() retrieves the quantified expression. In the resultant formula the bounded variables are free. The function Var(index, sort) creates a bounded/free variable with the given index and sort."
    ]
   },
   {
@@ -626,7 +626,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "When the more permissive pattern g(x) is used. Z3 proves the formula to be unsatisfiable. More restrive patterns minimize the number of instantiations (and potentially improve performance), but they may also make Z3 \"less complete\"."
+    "When the more permissive pattern g(x) is used. Z3 proves the formula to be unsatisfiable. More restrictive patterns minimize the number of instantiations (and potentially improve performance), but they may also make Z3 \"less complete\"."
    ]
   },
   {
diff --git a/examples/python/tutorial/jupyter/strategies.ipynb b/examples/python/tutorial/jupyter/strategies.ipynb
index a7f9df100..c5af684c9 100644
--- a/examples/python/tutorial/jupyter/strategies.ipynb
+++ b/examples/python/tutorial/jupyter/strategies.ipynb
@@ -33,7 +33,7 @@
     {
       "metadata": {},
       "cell_type": "markdown",
-      "source": "Tactics\nZ3 comes equipped with many built-in tactics. The command describe_tactics() provides a short description of all built-in tactics.\n\n describe_tactics()\nZ3Py comes equipped with the following tactic combinators (aka tacticals):\n\n* Then(t, s) applies t to the input goal and s to every subgoal produced by t.\n* OrElse(t, s) first applies t to the given goal, if it fails then returns the result of s applied to the given goal.\n* Repeat(t) Keep applying the given tactic until no subgoal is modified by it.\n* Repeat(t, n) Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than n.\n* TryFor(t, ms) Apply tactic t to the input goal, if it does not return in ms millisenconds, it fails.\n* With(t, params) Apply the given tactic using the given parameters.\n\nThe following example demonstrate how to use these combinators."
+      "source": "Tactics\nZ3 comes equipped with many built-in tactics. The command describe_tactics() provides a short description of all built-in tactics.\n\n describe_tactics()\nZ3Py comes equipped with the following tactic combinators (aka tacticals):\n\n* Then(t, s) applies t to the input goal and s to every subgoal produced by t.\n* OrElse(t, s) first applies t to the given goal, if it fails then returns the result of s applied to the given goal.\n* Repeat(t) Keep applying the given tactic until no subgoal is modified by it.\n* Repeat(t, n) Keep applying the given tactic until no subgoal is modified by it, or the number of iterations is greater than n.\n* TryFor(t, ms) Apply tactic t to the input goal, if it does not return in ms milliseconds, it fails.\n* With(t, params) Apply the given tactic using the given parameters.\n\nThe following example demonstrate how to use these combinators."
     },
     {
       "metadata": {