let mk_true = Bitvector.mk_one 1