~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

2023-04-21	use unique_ptr in Z3SolverImpl	Daniel Schemmel

2023-03-23	stats: rename numQueries/Queries -> SolverQueries, add Queries	Frank Busse

2022-08-26	Use true instead of Z3_TRUE (removed in z3 4.11.0)	Jerry James

2021-03-04	[Z3] Handle the case when interruption caught by Z3	Pavel Yatcheniy

2020-04-30	Moved header files that were placed directly in include/klee/ into ↵	Cristian Cadar
	appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30	Removed the Internal directory from include/klee	Cristian Cadar

2020-03-27	Ensure that temp_builder is used when adding constant array value assertion ↵	Daniel Grumberg
	constraints
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-11	Added Z3 options to the constraint solving category	Cristian Cadar

2018-10-30	Base time API upon std::chrono	Frank Busse
	This should not change the behaviour of KLEE and mimics the old API. - functions moved from util into time namespace - uses time points and time spans instead of double - CLI arguments now have the form "3h5min8us" Changed command line parameters: - batch-time (double to string) - istats-write-interval (double to string) - max-instruction-time (double to string) - max-solver-time (double to string) - max-time (double to string) - min-query-time-to-log (double to string) - seed-time (double to string) - stats-write-interval (double to string) - uncovered-update-interval (double to string) - added: log-timed-out-queries (replaces negative max-solver-time)
2018-10-23	refactor klee_open_output_file to return std::unique_ptr	Julian Büning
	and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
2018-09-20	Silence an uninitialized variable compiler warning (and a tiny formatting ↵	Cristian Cadar
	change)
2018-07-04	Fix compiler warnings if assertions are disabled	Martin Nowack

2018-05-09	Improve handling of constant array in Z3	Timotej Kapus

2017-06-02	hide backend solver declarations from public include	Hoang M. Le

2017-06-01	[Z3] Add `-debug-z3-verbosity=<N>` option which behaves like Z3's `-v:<N>` ↵	Dan Liew
	option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging.
2017-06-01	[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.	Dan Liew
	My discussions [1] with the Z3 team have revealed that `Z3_mk_simple_solver()` is the wrong solver to use. That solver basically runs the `simplify` tactic and then the `smt` tactic. This by-passes Z3's attempt to probe for different logics and apply its own specialized tactic. Using `Z3_mk_solver()` should be closer to the behaviour of the Z3 binary. This partially addresses #653. We still need to try rolling our own custom tactic. [1] https://github.com/Z3Prover/z3/issues/1035
2017-06-01	[Z3] In `getConstraintLog()` use a separate builder from that of the	Dan Liew
	solver. This is to avoid tampering with the cache of the builder the solver is using.
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] Add option to manually validate Z3 models.	Dan Liew
	This can be enabled by passing the command line option `-debug-z3-validate-models`. Although Z3 has a global parameter `model_validate` (off by default) I don't trust it so do the validation manually. This also means we can potentially do validation on a per Z3Solver instance basis rather than globally. When failing to validate a Z3 model the solver state and model are dumped to standard error.
2017-06-01	[Z3] Add the `-debug-z3-dump-queries=<path>` command line option. This	Dan Liew
	is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format.
2017-06-01	[Z3] Support another solver failure reason that Z3 might give. I'm going	Dan Liew
	to guess it means timeout but I'm not 100% sure about this.
2016-09-26	Modified logging information to steer the usage of klee_message, ↵	Andrea Mattavelli
	klee_warning, and klee_error
2016-05-25	add include in Z3Solver.cpp (did not compile with llvm-2.9)	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.