let find_model_example1() =
  begin
    printf "\nfind_model_example1\n";
    let ctx     = mk_context [||] in
    let x       = mk_bool_var ctx "x" in
    let y       = mk_bool_var ctx "y" in
    let x_xor_y = Z3.mk_xor ctx x y in
    Z3.assert_cnstr ctx x_xor_y;
    printf "model for: x xor y\n";
    check ctx Z3.L_TRUE;
    Z3.del_context ctx;
  end