The effects of an AssertFalse and a Terminal which branches to
<unreached> are very slightly different, because an AssertFalse can
reference uninitialised variables and a Terminal can't.  That means
that we can't combine the two states.  Stop doing so.
Rework the handling of InitialRegister side-effects so that they don't
force a state fork in the symbolic executor.
Revert 30fa2765ad91431d32fbcbf02f3dfae7d65897e7, because it's
completely the wrong way of fixing this.
Actually, merging AssertFalse and Terminal is fine.  Revert
49701753c0a1d86ef148ca2ef7d4ba8d9c3ddf38.
Do a better job of removing temporaries from the path condition as we
evaluate state machines.
Remove some crud from the symbolic execution engine.
Get rid of some redundant copying in the symbolic execution engine.
Dead code elimination.
Okay, this time the handling of uninit variables is correct.
StateMachine semantics are non-causal, so that if a variable is
initialised anywhere along a path then it has that value along the
entire path, even before the assignment which did the initialising.
That means that we can't say for sure that an uninitialised value is
undefined until we get to the end of the path, and so we have to do
the final filtering out at that point.  Anything which still depends
on undefined values at that point becomes smr_unreached, and we then
carefully filter out the smr_unreached states in a way which maintains
all of the paths which don't end in smr_unreached.