@michael-schwarz Brought up at todays Gobcon that as this is using the pathsensitivity functor, this may lead to a quadractic computational cost, as all iterations yet considered have to be considered again in each iteration.

Syntactic unrolling avoids this by introducing separate nodes and thus constraint unknowns for each iteration. Via that the solver can establish sensible fine-grained dependency structure and avoid recomputations of all iterations so many times.
Conceptually, it should be possible to also semantically create these unknowns in the constraint system construction for paths, which is a more general optimization we maybe should investigate. Similar explosion in paths can happen with must-locksets (as @karoliineh observed in some benchmark).

I'm closing this because we now have ideas for an alternative approach that should avoid the inefficiencies.