Hoare-Logic: Requirements for imperfect data types
No, when using Hoare logic properly, you make sure to account for integer overflow etc. and model the full semantics of the programming language.

It is possible to use Hoare logic along the lines you suggest, but the problem with that is that it invalidates all guarantees you might have hoped for.  Since the whole point of Hoare logic is to obtain guarantees, that seems rather counterproductive.

So if you are using Hoare logic for serious verification, you make sure that the Hoare triples accurately represent all elements of the language semantics, including integer overflow (if relevant).  For instance, part of the verification task might be to prove that integer overflow cannot happen; if you don't do that, then the Hoare triples need to account for that possibility.