let abstract_example() = 
  begin
    printf "\nabstract_example\n";
    let ctx          = mk_context [||] in
    let x            = mk_int_var ctx "x" in
    let x_decl       = Z3.get_app_decl ctx (Z3.to_app ctx x) in
    let y            = mk_int_var ctx "y" in
    let y_decl       = Z3.get_app_decl ctx (Z3.to_app ctx y) in
    let decls        = [| x_decl; y_decl |] in
    let a            = Z3.mk_string_symbol ctx "a" in
    let b            = Z3.mk_string_symbol ctx "b" in
    let names        = [| a; b |] in
    let str          = "(benchmark tst :formula (> a b))" in
    let f  = Z3.parse_smtlib_string_formula ctx str [||] [||] names decls in
    printf "formula: %s\n" (Z3.ast_to_string ctx f);

    let f2 = abstract ctx x 0 f in

    printf "abstracted formula: %s\n" (Z3.ast_to_string ctx f2);
    (* delete logical context *)
    Z3.del_context ctx;

  end