let mk_const c =
  Term.mk_const(Bv(Const(c)))