Detect the previous case — for loops where the iterator is a context variables — and throw a todo rather than hitting the invariant.