Fix typos in examples.

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";

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],

examples/python/mus/mss.py

@@ -118,11 +118,11 @@ def resolve_core(self, core):
 
    # 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 = []

examples/python/rc2.py

@@ -74,7 +74,7 @@ def compare(fw):
     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):            

examples/python/socrates.py

@@ -26,7 +26,7 @@
 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)))

examples/python/tutorial/html/advanced-examples.htm

@@ -505,7 +505,7 @@ <h2>Quantifiers</h2>
 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 @@ <h3>Patterns</h3>
 </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>

examples/python/tutorial/html/strategies-examples.htm

@@ -118,7 +118,7 @@ <h2>Tactics</h2>
 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>

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\"."
    ]
   },
   {

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": {