From efc1b1c297c531348ea9763e1f9f8bffb8db2a03 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 14 Oct 2025 16:31:04 +0000 Subject: [PATCH] Fix OCaml build error - use list instead of array for mk_datatype_sort Changed mk_sort_ref to pass empty list [] instead of empty array [||]. Changed mk_sort_ref_p to pass params list directly instead of converting to array. Z3native.mk_datatype_sort expects a list, not an array. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/ml/z3.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 57db13f9d..cc7294aba 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -909,14 +909,13 @@ struct mk_sort ctx (Symbol.mk_string ctx name) constructors let mk_sort_ref (ctx: context) (name:Symbol.symbol) = - Z3native.mk_datatype_sort ctx name 0 [||] + Z3native.mk_datatype_sort ctx name 0 [] let mk_sort_ref_s (ctx: context) (name: string) = mk_sort_ref ctx (Symbol.mk_string ctx name) let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) = - let param_array = Array.of_list params in - Z3native.mk_datatype_sort ctx name (List.length params) param_array + Z3native.mk_datatype_sort ctx name (List.length params) params let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) = mk_sort_ref_p ctx (Symbol.mk_string ctx name) params