> I read your code and it seems to me very clear that INT_MIN is exactly what the programmer intended.
Well, I'm the author and that's not what I intended.
I used INT_MAX as the initial value because it was a simple example. Imagine a case where the value happens to be equal to INT_MAX, and then you add 1 to it.
The fact that no result other than INT_MIN makes sense doesn't imply that INT_MIN does make sense. Saturation (having INT_MAX + 1 yield INT_MAX) or reporting an error seem equally sensible. We don't know which behavior is "correct" without knowing anything about the problem domain and what the program is supposed to do.
A likely scenario is that the programmer didn't intend the computation to overflow at all, but the program encountered input that the programmer hadn't anticipated.
INT_MAX + 1 commonly yields INT_MIN because typical hardware happens to work that way. It's not particularly meaningful in mathematical terms.
As for "natural properties", it violates "n + 1 > n". C integers are not, and cannot be, mathematical integers (unless you can restrict values to the range they support).