let prove ctx f is_valid =
  begin
    (* save the current state of the context *)
    Z3.push ctx;

    let not_f = Z3.mk_not ctx f in
    Z3.assert_cnstr ctx not_f;
    
    (match Z3.check_and_get_model ctx with
    | (Z3.L_FALSE,_) ->
        (* proved *)
        printf "valid\n";
        if not is_valid then exitf "unexpected result";
    | (Z3.L_UNDEF,m) ->
        (* Z3 failed to prove/disprove f. *)
        printf "unknown\n";
        (* m should be viewed as a potential counterexample. *)
        printf "potential counterexample:\n%s\n" (Z3.model_to_string ctx m);
        if is_valid then exitf "unexpected result";
    | (Z3.L_TRUE,m) ->
        (* disproved *)
        printf "invalid\n";
        (* the model returned by Z3 is a counterexample *)
        printf "counterexample:\n%s\n" (Z3.model_to_string ctx m);
        if is_valid then exitf "unexpected result";
    );
    (* restore context *)
    Z3.pop ctx 1;
  end