First off, when there are no loops, basically we're just doing straight abstract interpretation in arbitrary order. If we do a later block, then an earlier block, we just redo the later block and throw out the old results, but the end result is the same as if we went in the "perfect" order we'd do by hand.
Now consider a With loops, we actually need to analyze the loopbody more than once, even if we pick the best possible order. Because of the way states are merged, the first time, we analyze the body as if it is executed only once. The next time, like this (using our example lock()/unlock() analysis):we end up analyzing the body as if it is executed either once or twice. A fixed point is reached once further iterations produce no new behaviors.
[[ImageHere is an example of solving with a loop:treehydra-lock-cfg.png|right]][[Image:treehydra-lock-cfg-0.png|right]][[Image:treehydra-lock-cfg-1loop.png|right]]
