We discuss the inhabitation problem for a call-by-push-value-like language called BANG, a subsuming paradigm being able to encode, among others, call-by-name and call-by-value strategies of functional programming. The type specification uses a non-idempotent type system, which is able to capture quantitative properties about the dynamics of programs. As an application, we show how our general methodology can be used to derive inhabitation algorithms for different lambda-calculi that are encodable into BANG.