In an example introduced in #1131 , we reproduced an issue where a high offset causes a "wrapping around" behavior in CBMC.
There is more information on the test, but basically we should either enforce stricter checks than Rust (because of CBMC object bits limitations) or add these checks to CBMC itself.