Tweak dead code elimination a bit: if the only thing keeping a
variable live is an assertion then we should probably just treat that
variable as dead.  This can lead to use use-of-uninitialised in the
assertions, but that's not really a big deal.
Do a better job of stripping <unreached> states when we're told to
remove annotations.
Make slightly more use of the CDG by using it simplify withing states
as well as between them.
The various assertions which just enforce that the machine's control
flow predicates are consistent with the CFG structure are a bit
pointless.  Get rid of them.
Minor optimisation: if an expression is an address then that can
sometimes rule out some possible leaves, and hence make some internal
tests redundant.  Take advantage of that.
Extract a correct backtrace when we need to go across more than one
function.
Tweak the BDD normaliser so that we don't have bits which assert
BadPtr(x) and then immediately test LD(x).
Another tweak to BDD normalisation: make use of the fact that 0 == K
implies BadPtr(K).
Add a little debug crud to enumEvalPaths.
Kill off dead paths a little bit earlier during symbolic execution.
Turn down enumEvalPaths debug crud a little.
Redo symbolic exection so that it handles assertions (etc) by just
adding the asserted value to the path constraint, rather than creating
a whole new eval context for the case where we fail.
Rework the symbolic execution engine so that it defers aliasing
decisions for as long as possible by pushing them into the load result
exprbdd.