Add symmetrical "all_seen invariant failure" message

Now printed on both sides of a symmetrical invariant check.
Unforunately this isn't really just an internal invariant failure: it
can happen if the user setup causes the branches to be different on
different paths, such as with non-repeatable syscalls.
Update ITE parsing for x86 condition codes

Need triggered by introducing ITE expressions in ASMIR.
Re-instate a warning message when we fall back to some old code,
since that definitely is a bug (for instance it doesn't handle
smaller-than-word sizes correctly). Eventually that old code should
just go away.
The analogous ARM code probably still needs to be updated.
New option -finish-reasons-needed and related changes

Now that a -finish* condition doesn't immediately stop the path, it's
not a bug to run into more than one.
Another kind of generalization that can be useful is to require
multiple conditions before finishing exploration. The new -f-r-n option
gives a number of conditions: if that number are hit then the search
will really finish. (The old behavior corresponds to the default value
of 1.) I also considered negative conditions or requiring a
"conjunction" of conditions, which might also be useful, but this
seemed simplest.