Stop accepting truncated crash summaries.
Another canonicalisation step: encode aliasing stuff into the
verification condition, and then nuke the explicit aliasing table away
completely.
Split the oracle out into a ``true'' Oracle class and an
OracleInterface class.  The idea is that the OracleInterface just
handles aliasing queries, so is much easier to do a stub
implementation for.
For phase 2 canonicalisation we should pull the aliasing information
out of the crash summary, rather than using the oracle.  This is both
more accurate and more flexible (since we can now canonicalise memory
access identifiers in phase 1), and also quite a bit faster.
Replace the addresses of memory accessing expressions with fresh
variables, and then encode the actual pattern into the verification
condition.  This makes it easier to canonicalise the communication
patterns.
constify a few VexPtrs.  This is arguably somewhat deceptive, because
constifying the VexPtr doesn't constify the contained pointer, but
it's at least something.
Whoops: a missing aliasing table means that anything can alias, not
that nothing can.  That makes double-canonicalising the aliasing table
rather dangerous.  Stop doing so.
Add another canonicalisation pass which tries to remove bits of the
verification condition which aren't very interesting.
Tweak phase 1 canonicalisation a bit so that it simplifies Phi nodes
where we've lost the last assignment to one of the generations.
Split out phase 3 canonicalisation a little bit.
Minor refactoring.
Make sure we terminate lines following an abort().  This sometimes
means that you get redundant newlines, but that's not really that big
a deal, and it's worth it to make sure we don't lose important
messages.
Marginal improvement to phase 3 canonicaliser: remove clauses which
are underspecified by the structure of the verification condition.
Further extend the phase 3 canonicaliser with two new passes:

1) Equality substitution: if we have a clause which says ``tmp1 == tmp2''
then we can replace all instances of tmp2 with tmp1, and doing so will
usually improve the canonical-ness of the summary.  If we have multiple
such equalities available then we decide which to use based on the number
of times tmp1 and tmp2 appear in the summary, prefering to remove whichever
register appears most often.  That's a pretty arbitrary heuristic, but
seems to work well for at least a couple of interesting examples.

2) Underspecified clause removal: if a register is used in precisely
one place, there's a good chance that it's not really telling us
anything. E.g. if we have ``x == y + z + w'' then we can treat that
clause as defining z.  If there are no other mentions of z anywhere in
the summary (machines and verification condition) then that's a
redundant definition and we can remove the clause from the
verification condition in the same way that we'd remove dead
assignments from the machines in the summary.
printIRExpr() is really useful.  Make it available in more places.
Get rid of some annoying debug prints.
Put transformCrashSummary somewhere slightly more sensible.
Improve simplifier: arithmetic negation is its own inverse.
More work on phase 3 canonicalisation: we can use equalities to
eliminate registers from the machiens as well as from the verification
condition.
Make canonicalise_crash_summary3 GC-safe.