let find_model_example2() =
  begin
    printf "\nfind_model_example2\n";
    let ctx        = mk_context [||] in
    let x          = mk_int_var ctx "x" in
    let y          = mk_int_var ctx "y" in
    let one        = mk_int ctx 1 in
    let two        = mk_int ctx 2 in
    let y_plus_one = Z3.mk_add ctx [|y;one|] in
    let c1         = Z3.mk_lt ctx x y_plus_one in
    let c2         = Z3.mk_gt ctx x two in
    Z3.assert_cnstr ctx c1;
    Z3.assert_cnstr ctx c2;
    printf "model for: x < y + 1, x > 2\n";
    check ctx Z3.L_TRUE;

    (* assert not(x = y) *)
    let x_eq_y     = Z3.mk_eq ctx x y in
    let c3         = Z3.mk_not ctx x_eq_y in
    Z3.assert_cnstr ctx c3;
    printf "model for: x < y + 1, x > 2, not(x = y)\n";
    check ctx Z3.L_TRUE;
    Z3.del_context ctx;
  end