about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)Author
2017-07-08Corrected comment of Z3Solver classAndrew Santosa
2017-06-02hide backend solver declarations from public includeHoang M. Le
2017-06-02replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into Met...Hoang M. Le
2017-06-01[Z3] Remove unused include.Dan Liew
2017-06-01[Z3] Add `-debug-z3-verbosity=<N>` option which behaves like Z3's `-v:<N>` op...Dan Liew
2017-06-01[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.Dan Liew
2017-06-01[Z3] In `getConstraintLog()` use a separate builder from that of theDan Liew
2017-06-01[Z3] Implement API logging.Dan Liew
2017-06-01[Z3] Add option to manually validate Z3 models.Dan Liew
2017-06-01[Z3] Add the `-debug-z3-dump-queries=<path>` command line option. ThisDan Liew
2017-06-01[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializationsDan Liew
2017-06-01[Z3] Add assertions in Z3 builder to catch underflow with bad widths.Dan Liew
2017-06-01[Z3] Support another solver failure reason that Z3 might give. I'm goingDan Liew
2017-05-24llvm: make KLEE compile against LLVM 3.5 and 3.6Richard Trembecký
2017-03-23[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cppDan Liew
2017-03-23Add `AssignmentValidatingSolver`. It's purpose is to check any computedDan Liew
2017-03-03Using klee_message instead of llvm:errsCristian Cadar
2017-02-22klee: remove use of deprecated 'register'Jiri Slaby
2017-02-14Added error message when STP fails to fork.Cristian Cadar
2016-11-23Renamed .pc to .kquery (kleaver query)Eric Rizzi
2016-11-18[CMake] Remove use of tabs in `CMakeLists.txt` files.Dan Liew
2016-11-18[CMake] Re-express LLVM and KLEE library dependencies asDan Liew
2016-11-07Implement a CMake based build system for KLEE.Dan Liew
2016-10-27apply clang-formatHoang M. Le
2016-10-27update commentsHoang M. Le
2016-10-27upgrade to boolector-2.2.0 & remove the no longer needed aux array vectorHoang M. Le
2016-10-26move the query creation part into runAndGetCex() (to be consistent with runAn...Hoang M. Le
2016-10-26change signature of runAndGetCex() to match runAndGetCexForked()Hoang M. Le
2016-10-26remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop)Hoang M. Le
2016-09-29remove mimic_stp option and the associated ITE chain construction for shift o...Hoang M. Le
2016-09-26Modified logging information to steer the usage of klee_message, klee_warning...Andrea Mattavelli
2016-09-15Add ``-debug-cross-check-core-solver`` option to allow cross-checkingDan Liew
2016-08-06Fix to #445Andrea Mattavelli
2016-08-03fprintf: convert to klee_warningJiri Slaby
2016-07-31Merge pull request #422 from ccadar/div-zero-testCristian Cadar
2016-07-29Explicitely making division total in STP.Cristian Cadar
2016-07-09Fix variable shifting behavior with different sizesMartin Nowack
2016-07-08Support gzip-based compression of raw_outstreamsMartin Nowack
2016-06-28add assertions to check the pre-condition of bvVar*Shift that both operands h...Hoang M. Le
2016-06-27change bitwidth of expr_shpost in MetaSMTBuilder::constructSDivByConstant to ...Hoang M. Le
2016-06-10apply clang-formatHoang M. Le
2016-06-10remove now unused getShiftBits()Hoang M. Le
2016-06-10remove bitmasking shift amount in bvVarArithRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarLeftShiftHoang M. Le
2016-06-10remove bitmasking shift amount in constructAShrByConstant and make it return ...Hoang M. Le
2016-06-10remove bitmasking shift amount in bvRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvLeftShiftHoang M. Le
2016-06-10handle special cases of sdiv 1 and -1Hoang M. Le
2016-06-10update Makefile for metaSMTHoang M. Le
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 05:40:57 +0000