This execution feature allows users to place a bound on the number of iterations that a loop will execute. Each time a function is called, the included action is called to determine if the loops in that function should be bounded, and what their iteration bound should be.

The boolean argument indicates if we should generate proof obligations when we cut off loop execution. If true, loop cutoffs will generate proof obligations which will be provable only if the loop actually could not have executed that number of iterations. If false, the execution of loops will be aborted without generating side conditions.

Note that we compute a weak topological ordering on control flow graphs to determine loop heads and loop nesting structure. Loop bounds for inner loops are reset on every iteration through an outer loop.