From 1434c7d394d36ab53627b42d85dde50f8921a1cf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 9 Dec 2022 08:50:32 -0800
Subject: [PATCH] #6059

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/c++/z3++.h      | 21 +++++++++++++++++++++
 src/api/python/z3/z3.py |  2 +-
 2 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 553e71287..caf7ce07e 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1566,6 +1566,11 @@ namespace z3 {
         */
         expr substitute(expr_vector const& dst);
 
+        /**
+           \brief Apply function substitution by macro definitions.           
+        */
+        expr substitute(func_decl_vector const& funs, expr_vector const& bodies);
+
 
     class iterator {
             expr& e;
@@ -4059,6 +4064,22 @@ namespace z3 {
         return expr(ctx(), r);
     }
 
+    inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
+        array<Z3_ast> _dst(dst.size());
+        array<Z3_func_decl> _funs(funs.size());
+        if (dst.size() != funs.size()) {
+            Z3_THROW(exception("length of argument lists don't align"));
+            return expr(ctx(), nullptr);
+        }
+        for (unsigned i = 0; i < dst.size(); ++i) {
+            _dst[i] = dst[i];
+            _funs[i] = funs[i];
+        }
+        Z3_ast r = Z3_substitute_funs(ctx(), m_ast, dst.size(), _funs.ptr(), _dst.ptr());
+        check_error();
+        return expr(ctx(), r);
+    }
+
     typedef std::function<void(expr const& proof, expr_vector const& clause)> on_clause_eh_t;
 
     class on_clause {
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 72a3cd05f..c97cd2124 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8837,7 +8837,7 @@ def substitute_vars(t, *m):
     return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
 
 def substitute_funs(t, *m):
-    """Apply subistitution m on t, m is a list of pairs of a function and expression (from, to)
+    """Apply substitution m on t, m is a list of pairs of a function and expression (from, to)
     Every occurrence in to of the function from is replaced with the expression to.
     The expression to can have free variables, that refer to the arguments of from.
     For examples, see