Since c0241c1253bc6c65853cb9491e2e2e3cf5ae1ffa divisors in loop conditions are guarded by invariants.