Currently we don't even model control flow back edges in loops (because they will often lead to inference cycles). Once we have fixpoint iteration support in Salsa, we need to add these back edges and tests for them, including cases where we have to fallback to avoid runaway fixpoint iteration, e.g.:

x = 0
for _ in range(y):
    x += 1