Add basic implementation of Z3Builder and Z3Solver and Z3SolverImpl

which is based on the work of Andrew Santosa (see PR #295) but fixes
many bugs in that implementation. The implementation communicates
with Z3 via it's C API.

This implementation is based of the STPSolver and STPBuilder and so it
inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped
out some of the optimisations (constructMulByConstant,
constructSDivByConstant and constructUDivByConstant) that were used in
the STPBuilder because

* I don't trust them
* Z3 can probably do these for us in the future if we use the
 ``Z3_simplify()``

At a glance its performance seems worse than STP but future work can
look at improving this.

1 files changed, 2 insertions, 0 deletions

diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index debbe7d2..665cc842 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -480,6 +480,8 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     }
 
     if (WriteCVCs) {
+      // FIXME: If using Z3 as the core solver the emitted file is actually
+      // SMT-LIBv2 not CVC which is a bit confusing
       std::string constraints;
       m_interpreter->getConstraintLog(state, constraints, Interpreter::STP);
       llvm::raw_ostream *f = openTestFile("cvc", id);