let array_example1() =
  begin
    printf "\narray_example1\n";

    let ctx = mk_context [||] in

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

    let a1          = mk_var ctx "a1" array_sort in
    let a2          = mk_var ctx "a2" array_sort in
    let i1          = mk_var ctx "i1" int_sort in
    let i2          = mk_var ctx "i2" int_sort in
    let i3          = mk_var ctx "i3" int_sort in
    let v1          = mk_var ctx "v1" int_sort in
    let v2          = mk_var ctx "v2" int_sort in
    
    let st1         = Z3.mk_store ctx a1 i1 v1 in
    let st2         = Z3.mk_store ctx a2 i2 v2 in
    
    let sel1        = Z3.mk_select ctx a1 i3 in
    let sel2        = Z3.mk_select ctx a2 i3 in

    (* create antecedent *)
    let antecedent  = Z3.mk_eq ctx st1 st2 in

    (* create consequent: i1 = i3 or  i2 = i3 or select(a1, i3) = select(a2, i3) *)
    let ds = [|
        Z3.mk_eq ctx i1 i3;
        Z3.mk_eq ctx i2 i3;
        Z3.mk_eq ctx sel1 sel2;
      |] in

    let consequent  = Z3.mk_or ctx ds in

    (* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) *)
    let thm         = Z3.mk_implies ctx antecedent consequent in
    printf "prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n";
    printf "%s\n" (Z3.ast_to_string ctx thm);
    prove ctx thm true;

    Z3.del_context ctx;
  end