For my purposes, I would be happy with a way that I can specify constraints specifically in certain critical code sections, where I'd be happy to work around some false positives. Most other code could go on ignoring overflow as it does today.