I have just encountered this sentence:
Depending on the context, we may prefer to model integers as bitvectors rather than mathematical integers, since the Int type does not model overflow.
Another paper says something similar:
Overflows are a common source of programming errors, which makes it crucial to model them accordingly. In the theory of fixed-size bitvectors, overflow effects are directly modeled by the semantics of its function symbols and require no extra encoding constraints. These properties make bitvector logic a perfect fit for many verification purposes, especially in the field of low-level programming.