mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

fix: add substitute_funs to Expr module sig in z3.ml

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-11 19:21:31 +00:00 • committed by GitHub
parent 67ed39caa7
commit 4c5aef4287
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/ml/z3.ml
View file

@ -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