~cnx/klee - KLEE fork for patch differentiation testing

Age	Commit message (Collapse)	Author
2023-04-21	use unique_ptr all throughout the solver chain	Daniel Schemmel

2020-04-30	Removed the Internal directory from include/klee	Cristian Cadar

2019-09-03	Moved solver-related header files into a separate klee/Solver/ directory.	Cristian Cadar

2018-10-16	Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵	Cristian Cadar
	to have only solver options.
2017-06-02	hide backend solver declarations from public include	Hoang M. Le

2017-06-02	replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into ↵	Hoang M. Le
	MetaSMTSolver.cpp so that the backend headers only need to be included once there
2017-03-03	Using klee_message instead of llvm:errs	Cristian Cadar

2016-09-15	Add ``-debug-cross-check-core-solver`` option to allow cross-checking	Dan Liew
	with another solver. For example the core solver can be STP and the cross checking solver can be Z3. Unfortunately a few fragile tests don't pass when actually using this option.
2016-06-10	clean up metaSMT includes	Hoang M. Le

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.
2016-02-10	Add some of the basic plumbing required to support a Z3 solver in KLEE.	Dan Liew

2016-01-14	MetaSMT build fixes.	Dan Liew

2016-01-14	Make it possible to build KLEE without using STP and only MetaSMT.	Dan Liew
	The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency.
2016-01-12	Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing	Dan Liew
	a ``createCoreSolver()`` function. The solver used is set by the new ``--solver-backend`` command line argument. The default is STP. This change necessitated refactoring the MetaSMT stuff. That clearly didn't belong in the Executor! The MetaSMT command line option is now ``--metasmt-backend`` as this only picks the MetaSMT backend. In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed. Note I don't have MetaSMT built on my development machine so I don't know if the MetaSMT stuff even compiles...