let mk_xor a b = 
  Bitvector.mk_bitwise 1  a
    (Bitvector.mk_bitwise 1 b (mk_false) (mk_true))
    a