@spicyj Not sure if I follow, seeing as that is the exact condition for the while-loop, it could not possibly be false and trigger the invariant?