~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2019-09-03	Moved solver-related header files into a separate klee/Solver/ directory.	Cristian Cadar

2019-07-30	Consolidated Expr-related include files into a single include/klee/Expr ↵	Cristian Cadar
	directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE.
2019-03-13	Renamed --use-construct-hash to --use-construct-hash-stp and moved it and ↵	Cristian Cadar
	use-construct-hash-z3 to the expression building/printing category
2018-05-09	Improve handling of constant array in Z3	Timotej Kapus

2017-06-01	[Z3] Remove unused include.	Dan Liew

2017-06-01	[Z3] Implement API logging.	Dan Liew
	Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be logged to a file. The files logged by this option can be replayed by the `z3` binary (using its `-log` option). This is incredibly useful because it allows to exactly replay Z3's behaviour outside of KLEE.
2017-06-01	[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations	Dan Liew
	into `Z3Builder.cpp` so they can be called from in gdb.
2017-06-01	[Z3] Add assertions in Z3 builder to catch underflow with bad widths.	Dan Liew

2016-04-09	Generate unique STP and Z3 array names deterministically	Martin Nowack

2016-02-14	Handle Z3 API change between 4.4.1 and the current master branch	Dan Liew
	for the ``Z3_get_error_msg()`` function.
2016-02-14	Add basic implementation of Z3Builder and Z3Solver and Z3SolverImpl	Dan Liew
	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.