The thing that you didn't discuss in the above was the effect on the source code. Looking at your modified sources, I found it *significantly* harder to read your annotated version than the original. Basically every function and class was cluttered with irrelevant[1] conditions, which obscured the logic and the basic meaning of the code.
My reaction was just the same as Paul's. I read the modified source, and found that the invariant declarations made it *dramatically* harder to read. The ratio was almost exactly as I characterized in a recent note: 15 lines of pre/post-conditions on a 10 like function.
Like Paul, I understand the documentation and testing value of these, but they were highly disruptive to the readability of the functions themselves.
As a result of reading the example, I'd be somewhat less likely to use a DbC library, and much more strongly opposed to having one in the standards library (and aghast at the idea of dedicated syntax)