diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c
index 5696f5b89..50550106e 100644
--- a/examples/maxsat/maxsat.c
+++ b/examples/maxsat/maxsat.c
@@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z
 
 /**
    \brief Assert soft constraints stored in the given array.
-   This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
+   This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
    It will also return an array containing these fresh variables.
 */
 Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) 
@@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as
 
 /**
   \brief Finds the maximal number of assumptions that can be satisfied.
-  An assumption is any formula preceeded with the :assumption keyword.
+  An assumption is any formula preceded with the :assumption keyword.
   "Hard" constraints can be supported by using the :formula keyword.
   
   Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1b1820909..a355e0233 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -291,7 +291,7 @@ namespace z3 {
            \brief Return a tuple constructor.
            \c name is the name of the returned constructor,
            \c n are the number of arguments, \c names and \c sorts are their projected sorts.
-           \c projs is an output paramter. It contains the set of projection functions.
+           \c projs is an output parameter. It contains the set of projection functions.
         */
         func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 703105356..d466d2e77 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8327,7 +8327,7 @@ def prove(claim, **keywords):
         print(s.model())
 
 def _solve_html(*args, **keywords):
-    """Version of funcion `solve` used in RiSE4Fun."""
+    """Version of function `solve` used in RiSE4Fun."""
     s = Solver()
     s.set(**keywords)
     s.add(*args)
@@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords):
         print(s.model())
 
 def _solve_using_html(s, *args, **keywords):
-    """Version of funcion `solve_using` used in RiSE4Fun."""
+    """Version of function `solve_using` used in RiSE4Fun."""
     if __debug__:
         _z3_assert(isinstance(s, Solver), "Solver object expected")
     s.set(**keywords)
@@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords):
         print(s.model())
 
 def _prove_html(claim, **keywords):
-    """Version of funcion `prove` used in RiSE4Fun."""
+    """Version of function `prove` used in RiSE4Fun."""
     if __debug__:
         _z3_assert(is_bool(claim), "Z3 Boolean expression expected")
     s = Solver()