let mk_neg a = 
  Bitvector.mk_bitwise 1 a (mk_false) (mk_true)