Initial commit
Remove the note about CVC4 as the patch has been merged
Use a custom range for unconstrained arrays

This allows us to use non-standard expr widths and makes the SMT-LIB output
easier to read.
Fix a logic error when building candidate constraints with conditions

We were mistakenly testing the satisfiability of Cond -> E and Cond -> !E.
This is wrong; we need to test the validity of Cond -> !E and Cond -> E,
i.e. the satisfiability of !(Cond -> !E) and !(Cond -> E).
Make a start on Inst library
Finish the Inst library and port clients to it
Add some command line flags to assist in debugging
Use llvm-config --cppflags rather than --cxxflags

We don't necessarily want to inherit LLVM's warning options.
Remove an unused data structure
Fix the test used when forming a path condition from a conditional branch
Print names as comments alongside named insts
Simplify the extractor tests with a fixture
Filter candidate path conditions based on equivalence classes of variable sets
Fix Inst::operator< for the case where the operands are equal
Modify the update_deps.sh script to pass any remaining flags to CMake
When building equivalence classes, maintain a set of seen Insts

Helps avoid degenerate behavior with large self-referential insts.
Clang's CharInfoTest.cpp is a good test case for this.
Generate candidate queries on demand

The SMTLIB query builder has the same problem that I just fixed in the
equivalence class builder. This at least lets us look at the instructions
by not supplying a solver flag.
Roll KLEE to 5d8db05524f5216900e952c3e1fc2aac9c424391

This incorporates a fix in the SMTLIB printer for arrays with 1-bit ranges.
Include header files whose declarations are used
Support Z3