embeddLoopInvariant