let prove_example2() =
  begin
    printf "\nprove_example2\n";
    
    let ctx        = mk_context [||] in

    (* declare function g *)
    let int_sort    = Z3.mk_int_sort ctx in
    let g_name      = Z3.mk_string_symbol ctx "g" in
    let g           = Z3.mk_func_decl ctx g_name [|int_sort|] int_sort in

    (* create x, y, and z *)
    let x           = mk_int_var ctx "x" in
    let y           = mk_int_var ctx "y" in
    let z           = mk_int_var ctx "z" in

    (* create gx, gy, gz *)
    let gx          = mk_unary_app ctx g x in
    let gy          = mk_unary_app ctx g y in
    let gz          = mk_unary_app ctx g z in
    
    (* create zero *)
    let zero        = mk_int ctx 0 in

    (* assert not(g(g(x) - g(y)) = g(z)) *)
    let gx_gy       = Z3.mk_sub ctx [|gx;gy|] in
    let ggx_gy      = mk_unary_app ctx g gx_gy in
    let eq          = Z3.mk_eq ctx ggx_gy gz in
    let c1          = Z3.mk_not ctx eq in
    Z3.assert_cnstr ctx c1;

    (* assert x + z <= y *)
    let x_plus_z    = Z3.mk_add ctx [|x;z|] in
    let c2          = Z3.mk_le ctx x_plus_z y in
    Z3.assert_cnstr ctx c2;

    (* assert y <= x *)
    let c3          = Z3.mk_le ctx y x in
    Z3.assert_cnstr ctx c3;

    (* prove z < 0 *)
    let f           = Z3.mk_lt ctx z zero in
    printf "prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0\n";
    prove ctx f true;

    (* disprove z < -1 *)
    let minus_one   = mk_int ctx (-1) in
    let f           = Z3.mk_lt ctx z minus_one in
    printf "disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1\n";
    prove ctx f false;

    Z3.del_context ctx;
  end