From 2f33a346925f1957c698babe8bfa17c126e3d239 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 22:21:58 +0000 Subject: [PATCH] Fix OCaml build error in solver_get_levels 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 65cfad207..42c8fdd45 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1955,11 +1955,10 @@ struct let get_levels x literals = let n = List.length literals in - let levels = Array.make n 0 in let av = Z3native.mk_ast_vector (gc x) in List.iter (fun e -> Z3native.ast_vector_push (gc x) av e) literals; - Z3native.solver_get_levels (gc x) x av n levels; - levels + let level_list = Z3native.solver_get_levels (gc x) x av n in + Array.of_list level_list let congruence_root x a = Z3native.solver_congruence_root (gc x) x a