Skip to content

Commit ddb4956

Browse files
Merge pull request #8683 from Z3Prover/copilot/fix-build-error-z3
Fix OCaml binding call to solver_get_levels
2 parents 02b6aeb + 366b197 commit ddb4956

1 file changed

Lines changed: 2 additions & 3 deletions

File tree

src/api/ml/z3.ml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1955,11 +1955,10 @@ struct
19551955

19561956
let get_levels x literals =
19571957
let n = List.length literals in
1958-
let levels = Array.make n 0 in
19591958
let av = Z3native.mk_ast_vector (gc x) in
19601959
List.iter (fun e -> Z3native.ast_vector_push (gc x) av e) literals;
1961-
Z3native.solver_get_levels (gc x) x av n levels;
1962-
levels
1960+
let level_list = Z3native.solver_get_levels (gc x) x av n in
1961+
Array.of_list level_list
19631962

19641963
let congruence_root x a = Z3native.solver_congruence_root (gc x) x a
19651964

0 commit comments

Comments
 (0)