An outer loop's statically ranged accesses (the sieve's flags[i]) are
proved once per entry even when its body holds an inner loop. Versions
nest at most three deep and never inside their own copies, and fixed
checks only cover lengths a buffer can have, so an outer loop never pays
for a guard on an inner loop's unbounded counter.
Malte Ubl
0cf44e9265