Add a functional if-then-else expression type

In LibASMIR, Vine IR, and FuzzBALL's domain interface. We were already
using this in a bunch of places, and both VEX and STP support it,
so it makes sense to have it as a native expression type instead
of the awkward bitwise representation.
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.
Clear list of finishing reasons after each path

The previous change neglected to clear the list of reasons after each
path, so for instance you could hit a count of 2 by triggering the
same single condition on consecutive paths, which was not my intent.
Seeing that the state should be reset for each path reminded me
it was more logically part of the fragment machine object, so this
change also moves it there.
Start btor-as-stp.pl wrapper script

Stopgap for testing Boolector before we have native SMTLIB2 support.
Move table handling code to formula_manager

Introduce temporaries more aggressively to keep table formulas
smaller, and tweak the order in which trace messages are printed to
keep lines more separate.
Include patch for OCaml 4.02 cleanness

Several things that FuzzBALL uses are deprecated in OCaml 4.02;
unfortunately the replacements don't exist very far back, so we
can't easily fix the warnings without breaking compatibility.
Include the patch for the benefit of 4.02 users while we consider
the best way of handling this.
Implemented an SMT-LIB2 interface to STP.
Cosmetic cleanups to SMTLIB2 support

Keep the default solver as stp-external for now.
Tweak header comments on the new files.
Fix some trailing whitespace that Git dislikes
Add simplification rule for byte lost in >>

Can help for instance to reduce complexity when a word is used as a
shift buffer for bytes.
Add check_concolic_value debug routine

Add some code to check on the fly whether for each newly generated
temporary subformula, the concolic value of the subformula is
satisfiable under the path condition. This kind of check can help
track down places where the path condition is unexpectedly diverging
from the concolic input, or potentially if the formula construction
is making a mistake.

No command line option to enable it yet, since I don't know how
broadly useful it will be. For now, you just need to uncomment it.
Added push/pop support to the SMTLIB2 interface

Original patch from Matt Morehouse, but hand-applied because of
(whitespace?) divergences.

From 2f1873f846ce5bfe4731c27667c5122fc2d095e4 Mon Sep 17 00:00:00 2001
From: Matt Morehouse <mattmorehouse@gmail.com>
Date: Wed, 8 Oct 2014 10:09:36 -0500
Subject: [PATCH] Added push/pop support to the SMTLIB2 interface
Generalize SMTLIB2 support for CVC4

Original patch from Matt Morehouse, but hand-applied and further
changes: seemingly missing options_solver changes, rename_var for
re-flipping counterexample variable names.
The -stp-path option is now -solver-path, though the old name is
still recognized.
Use stderr instead of /dev/tty for update-git-version.pl messages

Some kinds of unattended builds can lack a controlling terminal.
Use \x in escaped strings, changes to table treatment

Implement our own version of escaped to go with unescaped, and prefer
\x00-style escapes instead of OCaml's C-incompatible decimal ones.
Add -no-table-stores to disable symbolic address range treatment
for stores.
Coordinate better between heuristics and -concolic-prob.
Add more newlines in -trace-tables output for predictability.
Implemented -trace-end-jump option.

The -trace-end-jump option takes the address of an indirect jump
as its value. Execution will stop after that jump, and the current
value of the program counter will be printed out.
Minor updates to finish condition handling

Print all the conditions at the end of the path.
Don't let later positive events override an earlier diqualifying one.
Add -extra-conditions-file option

For convenience when you have a lot of -extra-condition args.
Add -solver smtlib-batch

For SMTLIB2 solvers in non-incremental mode. The incremental
-solver smtlib will usually be more efficient when available, but a
batch mode can be helpful for debugging (making a single self-contained
query), and some solvers are batch-only.