let array_example3() =
  begin
    printf "\narray_example3\n";

    let ctx      = mk_context [||] in

    let bool_sort  = Z3.mk_bool_sort ctx in
    let int_sort   = Z3.mk_int_sort ctx in
    let array_sort = Z3.mk_array_sort ctx int_sort bool_sort in

    let (domain,range) = Z3.get_array_sort ctx array_sort in
    printf "domain: ";
    display_sort ctx stdout domain;
    printf "\n";
    printf "range:  ";
    display_sort ctx stdout range;
    printf "\n";

    if (not (Z3.is_eq_sort ctx int_sort domain)) ||
       (not (Z3.is_eq_sort ctx bool_sort range)) then
        exitf "invalid array type";
    Z3.del_context ctx;
  end