Native support in CBMC for saturating add/sub was introduced in diffblue/cbmc#6647

The current implementation does not use that and seems to work well, but we may consider emitting CBMC ireps instead for various reasons (cleaner code, performance, etc.).