let bitvector_example1() =
  begin
    printf "\nbitvector_example1\n";
    
    let ctx       = mk_context [||] in
    
    let bv_sort   = Z3.mk_bv_sort ctx 32 in
    
    let x           = mk_var ctx "x" bv_sort in
    let zero        = Z3.mk_numeral ctx "0" bv_sort in
    let ten         = Z3.mk_numeral ctx "10" bv_sort in
    let x_minus_ten = Z3.mk_bvsub ctx x ten in
    (* bvsle is signed less than or equal to *)
    let c1          = Z3.mk_bvsle ctx x ten in
    let c2          = Z3.mk_bvsle ctx x_minus_ten zero in
    let thm         = Z3.mk_iff ctx c1 c2 in
    printf "disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n";
    prove ctx thm false;
    
    Z3.del_context ctx;
  end