From 4c5aef42878dc2eca99cc4736aec9376225ace36 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 11 Apr 2026 19:21:31 +0000
Subject: [PATCH] fix: add substitute_funs to Expr module sig in z3.ml

The internal sig...end block in z3.ml (the module type declaration for Expr)
was missing val substitute_funs, causing OCaml compiler error:
  The value substitute_funs is required but not provided

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c6662702-46a3-4aa0-b225-d6b73c2a2505

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/ml/z3.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 37ebcc44e..261bc2f3c 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -475,6 +475,7 @@ sig
   val substitute : expr -> expr list -> expr list -> expr
   val substitute_one : expr -> expr -> expr -> expr
   val substitute_vars : expr -> expr list -> expr
+  val substitute_funs : expr -> FuncDecl.func_decl list -> expr list -> expr
   val translate : expr -> context -> expr
   val to_string : expr -> string
   val is_numeral : expr -> bool