In symbolic execution, every branch forks the engine: the
true path and the
false path are both explored independently.
Inside a loop this causes exponential explosion — 2N paths after N iterations.
Control-flow merging linearizes the loop body into a single combined block
that computes both outcomes and picks the right one via a
select,
keeping a single symbolic state throughout.
Drag the slider (or press Play) to watch the divergence.
Loop iterations
3
Without merging: 8 paths
With merging: 1 path
Without Merging
Paths fork at every conditional — never joined
True branch
False branch
Loop / exit
With Merging — linearized dataflow
Both paths computed inside one block; select picks the result