let mk_disj a b = 
  Bitvector.mk_bitwise 1 a (mk_true) b