diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in
index 9e946aa7f..9c4b464c2 100644
--- a/doc/z3api.cfg.in
+++ b/doc/z3api.cfg.in
@@ -704,10 +704,13 @@ INPUT_ENCODING         = UTF-8
 FILE_PATTERNS          = website.dox \
                          z3_api.h \
                          z3_algebraic.h \
+                         z3_ast_containers.h \
+                         z3_fixedpoint.h \
+                         z3_fpa.h \
+                         z3_interp.h \
+                         z3_optimization.h \
                          z3_polynomial.h \
                          z3_rcf.h \
-                         z3_interp.h \
-                         z3_fpa.h \
                          z3++.h \
                          @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 84a80ddf7..dbd8019c4 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -50,6 +50,7 @@ from fractions import Fraction
 import sys
 import io
 import math
+import copy
 
 if sys.version < '3':
     def _is_int(v):
@@ -288,6 +289,9 @@ class AstRef(Z3PPObject):
         if self.ctx.ref() is not None:
            Z3_dec_ref(self.ctx.ref(), self.as_ast())
 
+    def __deepcopy__(self, memo={}):
+        return _to_ast_ref(self.ast, self.ctx)
+
     def __str__(self):
         return obj_to_string(self)
 
@@ -4357,6 +4361,11 @@ class Datatype:
         self.name         = name
         self.constructors = []
 
+    def __deepcopy__(self, memo={}):
+        r = Datatype(self.name, self.ctx)
+        r.constructors = copy.deepcopy(self.constructors)
+        return r
+
     def declare_core(self, name, rec_name, *args):
         if __debug__:
             _z3_assert(isinstance(name, str), "String expected")
@@ -4647,11 +4656,17 @@ class ParamsRef:
 
     Consider using the function `args2params` to create instances of this object.
     """
-    def __init__(self, ctx=None):
+    def __init__(self, ctx=None, params=None):
         self.ctx    = _get_ctx(ctx)
-        self.params = Z3_mk_params(self.ctx.ref())
+        if params is None:
+            self.params = Z3_mk_params(self.ctx.ref())
+        else:
+            self.params = params
         Z3_params_inc_ref(self.ctx.ref(), self.params)
 
+    def __deepcopy__(self, memo={}):
+        return ParamsRef(self.ctx, self.params)
+
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_params_dec_ref(self.ctx.ref(), self.params)
@@ -4711,6 +4726,9 @@ class ParamDescrsRef:
         self.descr  = descr
         Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
 
+    def __deepcopy__(self, memo={}):
+        return ParamsDescrsRef(self.descr, self.ctx)
+
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
@@ -4772,6 +4790,9 @@ class Goal(Z3PPObject):
             self.goal   = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
         Z3_goal_inc_ref(self.ctx.ref(), self.goal)
 
+    def __deepcopy__(self, memo={}):
+        return Goal(False, False, False, self.ctx, self.goal)
+
     def __del__(self):
         if self.goal is not None and self.ctx.ref() is not None:
             Z3_goal_dec_ref(self.ctx.ref(), self.goal)
@@ -5034,6 +5055,9 @@ class AstVector(Z3PPObject):
             self.ctx    = ctx
         Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
 
+    def __deepcopy__(self, memo={}):
+        return AstVector(self.vector, self.ctx)
+
     def __del__(self):
         if self.vector is not None and self.ctx.ref() is not None:
             Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector)
@@ -5169,6 +5193,9 @@ class AstMap:
             self.ctx    = ctx
         Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
 
+    def __deepcopy__(self, memo={}):
+        return AstMap(self.map, self.ctx)
+
     def __del__(self):
         if self.map is not None and self.ctx.ref() is not None:
             Z3_ast_map_dec_ref(self.ctx.ref(), self.map)
@@ -5284,6 +5311,9 @@ class FuncEntry:
         self.ctx   = ctx
         Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
 
+    def __deepcopy__(self, memo={}):
+        return FuncEntry(self.entry, self.ctx)
+
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
@@ -5390,6 +5420,9 @@ class FuncInterp(Z3PPObject):
         if self.f is not None:
             Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
 
+    def __deepcopy__(self, memo={}):
+        return FuncInterp(self.f, self.ctx)
+
     def __del__(self):
         if self.f is not None and self.ctx.ref() is not None:
             Z3_func_interp_dec_ref(self.ctx.ref(), self.f)
@@ -5500,6 +5533,9 @@ class ModelRef(Z3PPObject):
         self.ctx   = ctx
         Z3_model_inc_ref(self.ctx.ref(), self.model)
 
+    def __deepcopy__(self, memo={}):
+        return ModelRef(self.m, self.ctx)
+
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_model_dec_ref(self.ctx.ref(), self.model)
@@ -5776,6 +5812,9 @@ class Statistics:
         self.ctx   = ctx
         Z3_stats_inc_ref(self.ctx.ref(), self.stats)
 
+    def __deepcopy__(self, memo={}):
+        return Statistics(self.stats, self.ctx)
+
     def __del__(self):
         if self.ctx.ref() is not None:
            Z3_stats_dec_ref(self.ctx.ref(), self.stats)
@@ -5910,6 +5949,9 @@ class CheckSatResult:
     def __init__(self, r):
         self.r = r
 
+    def __deepcopy__(self, memo={}):
+        return CheckSatResult(self.r)
+
     def __eq__(self, other):
         return isinstance(other, CheckSatResult) and self.r == other.r
 
@@ -5949,6 +5991,9 @@ class Solver(Z3PPObject):
             self.solver = solver
         Z3_solver_inc_ref(self.ctx.ref(), self.solver)
 
+    def __deepcopy__(self, memo={}):
+        return Solver(self.solver, self.ctx)
+
     def __del__(self):
         if self.solver is not None and self.ctx.ref() is not None:
             Z3_solver_dec_ref(self.ctx.ref(), self.solver)
@@ -6369,6 +6414,9 @@ class Fixedpoint(Z3PPObject):
         Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
         self.vars = []
 
+    def __deepcopy__(self, memo={}):
+        return FixedPoint(self.fixedpoint, self.ctx)
+
     def __del__(self):
         if self.fixedpoint is not None and self.ctx.ref() is not None:
             Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
@@ -6743,6 +6791,9 @@ class Optimize(Z3PPObject):
         self.optimize = Z3_mk_optimize(self.ctx.ref())
         Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
 
+    def __deepcopy__(self, memo={}):
+        return Optimize(self.optimize, self.ctx)
+
     def __del__(self):
         if self.optimize is not None and self.ctx.ref() is not None:
             Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
@@ -6895,6 +6946,9 @@ class ApplyResult(Z3PPObject):
         self.ctx    = ctx
         Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
 
+    def __deepcopy__(self, memo={}):
+        return ApplyResult(self.result, self.ctx)
+
     def __del__(self):
         if self.ctx.ref() is not None:
             Z3_apply_result_dec_ref(self.ctx.ref(), self.result)
@@ -7023,6 +7077,9 @@ class Tactic:
                 raise Z3Exception("unknown tactic '%s'" % tactic)
         Z3_tactic_inc_ref(self.ctx.ref(), self.tactic)
 
+    def __deepcopy__(self, memo={}):
+        return Tactic(self.tactic, self.ctx)
+
     def __del__(self):
         if self.tactic is not None and self.ctx.ref() is not None:
             Z3_tactic_dec_ref(self.ctx.ref(), self.tactic)
@@ -7295,6 +7352,9 @@ class Probe:
                 raise Z3Exception("unknown probe '%s'" % probe)
         Z3_probe_inc_ref(self.ctx.ref(), self.probe)
 
+    def __deepcopy__(self, memo={}):
+        return Probe(self.probe, self.ctx)
+
     def __del__(self):
         if self.probe is not None and self.ctx.ref() is not None:
             Z3_probe_dec_ref(self.ctx.ref(), self.probe)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 45065f856..b862884c9 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -48,6 +48,7 @@ DEFINE_TYPE(Z3_rcf_num);
 /*@{*/
 
 /** @name Types
+    @{
 
    Most of the types in the C API are opaque pointers.
 
@@ -5238,7 +5239,6 @@ extern "C" {
        def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
     */
     Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
-    /*@}*/
 
     /**
        \brief Return a string describing the given error code.
@@ -5349,6 +5349,10 @@ extern "C" {
 
     /**
        \brief Add a new formula \c a to the given goal.
+        Conjunctions are split into separate formulas.
+        If the goal is \c false, adding new formulas is a no-op.
+        If the formula \c a is \c true, then nothing is added.
+        If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.
 
        def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST)))
     */
diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
index 795b4b8fd..f49e1b9ce 100644
--- a/src/api/z3_optimization.h
+++ b/src/api/z3_optimization.h
@@ -75,7 +75,7 @@ extern "C" {
        \brief Add a maximization constraint.
        \param c - context
        \param o - optimization context
-       \param a - arithmetical term
+       \param t - arithmetical term
        def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
     unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
@@ -84,7 +84,7 @@ extern "C" {
        \brief Add a minimization constraint.
        \param c - context
        \param o - optimization context
-       \param a - arithmetical term
+       \param t - arithmetical term
 
        def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */