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!