bearophile wrote:
I think you are missing about half of the ideas tied to this nonnullable discussion. I suggest you to read the linked article about Spec#.
"The current version of the Spec# program verifier does not check for arithmetic overflow." Oh well!
