14b790b0cf
The code does the right thing, but the compiler is unable to figure it out. All paths that use that variable use the same invariant.