mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 15:47:29 +00:00
Code Activity

Fix OCaml build error - use list instead of array for mk_datatype_sort

Browse source 
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>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-14 16:31:04 +00:00
parent 9a8df8f80d
commit efc1b1c297
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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