No, it does not. This is mentioned as a limitation in the paper (it does, however, handle things like integer overflows correctly). I believe with some suitab

No, it does not. This is mentioned as a limitation in the paper (it does, however, handle things like integer overflows correctly). I believe with some suitable extensions, it would be possible to prove invariants like this as well, but IMO functional correctness is a pretty good start!