Symbolic execution can fork a state when a branch depends on symbolic input
and both outcomes are feasible. The
true branch and the
false branch are then explored independently.
With two feasible choices at each iteration, this simplified example has
2N possible paths after N iterations.
In this example, control-flow merging replaces the branch with a
combined block that computes both outcomes and uses
select
to choose the appropriate result. This avoids state forking at that branch.
Move the slider or press Play to compare the two versions.
Loop iterations
3
Without merging 8 symbolic states
With merging 1 symbolic state
Without merging
Symbolic states fork at the branch and remain separate in this example.
True branch
False branch
Loop / exit
With merging
The combined block computes both outcomes. select chooses the appropriate result.