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