`Model.get_decls` has "index out of bounds" error in OCaml bindings

[brandonzstride]

Bug

Model.get_decls crashes with an out of bounds message when both functions and constants are present.

This issue affects only the OCaml API of Z3.

Example

Here is a reproducing example:

let ctx = Z3.mk_context []
let solver = Z3.Solver.mk_solver ctx None
let int_sort = Z3.Arithmetic.Integer.mk_sort ctx 

let f = Z3.FuncDecl.mk_func_decl ctx (Z3.Symbol.mk_string ctx "f") [int_sort] int_sort 
let x = Z3.Expr.mk_const ctx (Z3.Symbol.mk_string ctx "x") int_sort 
let fx = Z3.FuncDecl.apply f [x]

let eq = Z3.Boolean.mk_eq ctx fx x

let () =
  match Z3.Solver.check solver [eq] with
  | Z3.Solver.SATISFIABLE ->
      let model = Option.get (Z3.Solver.get_model solver) in
      Printf.printf "Model:\n%s\n" (Z3.Model.to_string model);
      let decls = Z3.Model.get_decls model in (* Error happens here *)
      List.iter (fun d ->
        let sym = Z3.FuncDecl.get_name d in
        Printf.printf "Decl: %s\n" (Z3.Symbol.to_string sym)
      ) decls
  | _ -> failwith "unexpected UNSAT"

The bugged behavior is as follows.

Model:
(define-fun x () Int
  2)
(define-fun f ((x!0 Int)) Int
  2)
Fatal error: exception Z3.Error("index out of bounds")

The following is the expected behavior.

Model:
(define-fun x () Int
  2)
(define-fun f ((x!0 Int)) Int
  2)
Decl: f
Decl: x

Proposed fix

I am submitting a PR to fix this issue. One can expect it very soon.