Various fixes to phase 3 canonicalisation.
findTargetRegisters is the most expensive part of phase 3
canonicalisation.  It should therefore be run at the end, once the
simpler canonicalisation passes have all bottomed out.
Add another case to clauseUnderspecified().
Hackety hackety hack: our IRExpr parser can't cope with redundant
brackets, which is what you get if you have an assoc with a single
argument.  Rather than fixing the parser, tweak the pretty printer so
that we don't print the redundant brackets.
Add a new method on side effects, inputExpressions(), which goes and
finds all of the expressions which the side effect will have to
evaluate before doing anything.
Yet another improvement to clauseUnderspecified.
Stop treating timeouts as hard errors, to make the real hard errors
a bit more obvious.
inputExpressions() is more useful if it doesn't contain NULL pointers.
Make it so.
Maintain type correctness during phase 3 equality substitution.
More correct version of clauseUnderdetermined.  x < y is only
underdetermined if both x and y are.  Otherwise, you might, say, have
y equal to zero, in which case no value of x could possibly make the
expression true (for unsigned <; the signed operator has an analogous
problem).
Minor tweak to simplifier: x < 0 is always false for unsigned < 0, and
0 < x is just x != 0.
Empty atomic blocks are a bit pointless.  Get rid of them.
Individual side effects are all atomic, so there's not much point in
wrapping them in START_ATOMIC/END_ATOMIC blocks.  Have the optimiser
remove these wherever possible.
Extend the underspecification analysis with a kind of conditional
underspecification, SSA-style analysis.

The idea is that if the verification condition V is a function of
boolean variables X, Y and Z then we should be able to do a case split
on any of them, X say, and re-express the condition as
(X && V(X=true)) || (!X && V(X=false)).  Once you've done that, you
can split Y into Y_{X=true} and Y_{X=false}, and likewise Z, in effect
treating all of our free variables as functions of X.  That then makes
all of the existing redundant clause and underspecified clause
canonicalisation passes much more powerful.

(You need to be careful that Y and Z are actually free, but,
fortunately, the existing targetRegisters set provides almost
precisely the right rules for doing so.)

There are a couple of ways of looking at this:

1) Most obviously, it captures certain conditional independence
   properties of the program.  It might by, for instance, that we're
   only interested in variable X and V is

   ((X == Y) || (X == Z)) && (Y != Z)

   If Y is true then that becomes

   ((X == true) || (X == Z)) && (true != Z)
   ->
   ((X == true) || (X == Z)) && (Z == false)
   ->
   (X == true) || (X == false)
   ->
   true.

   Likewise, if Y is false then it becomes

   ((X == false) || (X == Z)) && (false != Z)
   ->
   ((X == false) || (X == Z)) && (Z == true)
   ->
   (X == false) || (X == true)
   ->
   true

   V is therefore independent of X, conditional on Y, and so isn't
   really telling us anything.

   We can therefore re-express V as just

   (Y && true) || (!Y && true)
   ->
   Y || !Y
   ->
   true

   The case where we split on X first is somewhat more subtle, because
   as soon as you do the substitution you find that every clause is
   redundant (because it doesn't mention any target values), but
   produces essentially the same result.

2) It's also quite a lot like SSA.  The point is that the direct
   expression of the condition mixes up the values of Y for the
   different values of X, even though they're logically unrelated.  By
   splitting them up again we open up lots of other opportunities
   for optimisation.
Fix silly bug in equality substitution to do with use of nested add
operations.
Marginal improvement in simplifier: replace CmpLE operators with ==
and CmpLT operators.
Whoops: fix an unfortunate NULL dereference on a timeout path.
Fix another timeout path.
Fix yet another timeout path.
Fix stupid infinite loop in optimiseStateMachine().