let assert_inj_axiom ctx f i = 
  begin
    let sz = Z3.get_domain_size ctx f in
    if i >= sz then exitf "failed to create inj axiom";
    
    (* declare the i-th inverse of f: finv *)
    let finv_domain = Z3.get_range ctx f in
    let finv_range  = Z3.get_domain ctx f i in
    let finv        = Z3.mk_fresh_func_decl ctx "inv" [|finv_domain|] finv_range in

    (* allocate temporary arrays *)
    (* fill types, names and xs *)
    let types       = Z3.get_domains ctx f in
    let names       = Array.init sz (Z3.mk_int_symbol ctx) in
    let xs          = Array.init sz (fun j->Z3.mk_bound ctx j (types.(j))) in

    (* create f(x_0, ..., x_i, ..., x_{n-1}) *)
    let fxs         = Z3.mk_app ctx f xs in

    (* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) *)
    let finv_fxs    = mk_unary_app ctx finv fxs in

    (* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i *)
    let eq          = Z3.mk_eq ctx finv_fxs (xs.(i)) in

    (* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier *)
    let p           = Z3.mk_pattern ctx [|fxs|] in
    printf "pattern: %s\n" (Z3.pattern_to_string ctx p);
    printf "\n";

    (* create & assert quantifier *)
    let q           = Z3.mk_forall ctx 
                                   0 (* using default weight *)
                                   [|p|] (* the " of patterns *)
                                   types
                                   names
                                   eq
    in
    printf "assert axiom:\n%s\n" (Z3.ast_to_string ctx q);
    Z3.assert_cnstr ctx q;
  end