Fix a silly off-by-one in minimal_direct's driver loop.
At the moment, when we try to pick a root for a cycle, we try to pick
a true target.  That turns out to be pretty much pessimal.  What we
should be doing is picking the node *furthest* from a true
instruction, so as to preserve as much information as possible.
Special case: BadPtr(k+RSP) is always false, provided that RSP is a
constant.
Minor improvement to debug logging.
Whoops: getStoreCFGs loop unroller is completely borked in the case
where the root of the CFG isn't a true instruction.  Fix it.
Whoops: don't stop building the store machine just because we find a
library function we don't know about.  This isn't really correct
(ignoring the function completely really isn't a great strategy), but
it's at least ever so slightly less incorrect.
Implement the time() library function.
If we decide to elide a library call then we need to make sure that we
fix up the stack afterwards, or else very bad things happen.
Tweak the way we build concatenated machines for deriving W_atomic
constraint.  We only need to care about the case where the store
machine reaches <crash>, which means turning any branches to <survive>
in the store machine into branches to <crash> in the composite
machine.
Tweak removeRedundantStores() to remove the earlier of two stores to
the same address.
Whoops.  Make the conversion of Xor1 operators to ANF less broken.
Add another debug flag to survivalConstraintIfExecutedAtomically().
Marginal improvement to the sat checker.  When we have to use the ND
chooser, we have a choice about whether we take the positive sense
first or the negative.  Try to be a bit more sensible about it.
Add another test, and gubbins to run it all the way from the beginning
to the end of minimal_direct automatically.
Add a thing to allow us to test the store CFG unroller in isolation.
Rework the way we handle node labellings when build store CFGs, so as
to make it a bit clearer and easier to explain, and also a bit faster.
Rework the way we find roots of store CFGs.  Previously, the only
requirement was that every CFG node be reachable from at least one
root.  That turns out to be inadequate, because some of the edges in
the CFG aren't actually possible.

e.g. suppose you have a program like this:

l1: loc = a;
l2: for (i = 0; i < 1000000; i++)
l3:    nop;
l4: loc = b;

Now the CFG shows a simple path l1 -> l2 -> l4, so l1 and l4 will be
grouped together.  However, it's not actually possible to do that,
because you have to go round the loop 1000000 times.  The unroll won't
be able to cover that many instructions, though, so we'll in effect
only consider running the loop up to N_w times, which means that we'll
conclude that l4 can never run.  The only real fix to this is to make
l4 a root of the CFG as well.

We can still backtrack roots where its unambiguous to do so, though.
If we've selected X as a root, and Y is definitely executed
immediately before X, we can safely use Y as a root instead of X.
Because we know that prior to executing X we must have used the Y->X
edge, we know that if you can eliminate the Y->X edge then X is never
executable, so we're fine.
The store CFG backtracker isn't really there to extend the CFG (any
more), but instead to find sensible places to place roots.  It's
therefore not a good idea to exit just because we discover that
we can't expand the CFG any further.
Simplify test case slightly.
Add another couple of special cases to clauseUnderspecified().