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

    (* create a big number *)
    let int_sort   = Z3.mk_int_sort ctx in
    let big_number = Z3.mk_numeral ctx "1000000000000000000000000000000000000000000000000000000" int_sort in
    
    (* create number 3 *)
    let three      = Z3.mk_numeral ctx "3" int_sort in

    (* create x *)
    let x_sym      = Z3.mk_string_symbol ctx "x" in
    let x          = Z3.mk_const ctx x_sym int_sort in

    (* assert x >= " *)
    let c1         = Z3.mk_ge ctx x big_number in
    printf "assert: x >= 'big number'\n";
    Z3.assert_cnstr ctx c1;

    (* create a backtracking point *)
    printf "push\n";
    Z3.push ctx;

    (* assert x <= 3 *)
    let c2         = Z3.mk_le ctx x three in
    printf "assert: x <= 3\n";
    Z3.assert_cnstr ctx c2;

    (* context is inconsistent at this point *)
    check2 ctx Z3.L_FALSE;

    (* backtrack: the constraint x <= 3 will be removed, since it was
       asserted after the last push. *)
    printf "pop\n";
    Z3.pop ctx 1;

    (* the context is consistent again. *)
    check2 ctx Z3.L_TRUE;

    (* new constraints can be asserted... *)
    
    (* create y *)
    let y_sym      = Z3.mk_string_symbol ctx "y" in
    let y          = Z3.mk_const ctx y_sym int_sort in

    (* assert y > x *)
    let c3         = Z3.mk_gt ctx y x in
    printf "assert: y > x\n";
    Z3.assert_cnstr ctx c3;

    (* the context is still consistent. *)
    check2 ctx Z3.L_TRUE;
    
    Z3.del_context ctx;
  end