let quantifier_example1() =
  begin
    printf "\nquantifier_example1\n";

    (* If quantified formulas are asserted in a logical context, then
       the model produced by Z3 should be viewed as a potential model.

    *)
    let ctx = mk_context [| |] in

    (* declare function f *)
    let int_sort    = Z3.mk_int_sort ctx in
    let f_name      = Z3.mk_string_symbol ctx "f" in
    let f           = Z3.mk_func_decl ctx f_name [|int_sort; int_sort|] int_sort in
  
    (* assert that f is injective in the second argument. *)
    assert_inj_axiom ctx f 1;
    
    (* create x, y, v, w, fxy, fwv *)
    let x           = mk_int_var ctx "x" in
    let y           = mk_int_var ctx "y" in
    let v           = mk_int_var ctx "v" in
    let w           = mk_int_var ctx "w" in
    let fxy         = mk_binary_app ctx f x y in
    let fwv         = mk_binary_app ctx f w v in
    
    (* assert f(x, y) = f(w, v) *)
    let p1          = Z3.mk_eq ctx fxy fwv in
    Z3.assert_cnstr ctx p1;

    (* prove f(x, y) = f(w, v) implies y = v *)
    let p2          = Z3.mk_eq ctx y v in
    printf "prove: f(x, y) = f(w, v) implies y = v\n";
    prove ctx p2 true;

    (* disprove f(x, y) = f(w, v) implies x = w *)
    (* using check2 instead of prove *)
    let p3          = Z3.mk_eq ctx x w in
    let not_p3      = Z3.mk_not ctx p3 in
    Z3.assert_cnstr ctx not_p3;
    printf "disprove: f(x, y) = f(w, v) implies x = w\n";
    printf "that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable\n";
    check2 ctx Z3.L_UNDEF;
    Printf.printf
        "reason for last failure: %d (7 = quantifiers)\n" 
        (if Z3.get_search_failure(ctx) = Z3.QUANTIFIERS then 7 else -1);


    Z3.del_context ctx;
  end