let mk_const c = Term.App.mk_const(Sym.Bv.mk_const c)