about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)Author
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
2016-06-10clean up metaSMT includesHoang M. Le
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
2016-04-19Merge pull request #369 from MartinNowack/fix_determ_solver_arrayMartinNowack
2016-04-17Merge pull request #359 from delcypher/fix_indep_solver_bugCristian Cadar
2016-04-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
2016-03-23Refactoring of conditional flush into own function.Martin Nowack
2016-03-23Fix comment + Clang FormattingMartin Nowack
2016-03-23Add option to log partial solver queries before calling itMartin Nowack
2016-03-22Properly assert that an assignment computed inDan Liew
2016-03-22Try to fix #348Dan Liew
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-14Handle Z3 API change between 4.4.1 and the current master branchDan Liew
2016-02-14Add basic implementation of Z3Builder and Z3Solver and Z3SolverImplDan Liew
2016-02-10Add some of the basic plumbing required to support a Z3 solver in KLEE.Dan Liew
2016-01-14MetaSMT build fixes.Dan Liew
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
2016-01-12Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providingDan Liew
2016-01-12Drop unnecessary ``#include``s from Solver.cpp.Dan Liew
2016-01-12Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp intoDan Liew
2016-01-12[NFC] Refactor STPSolver and STPSolverImpl out of Solver.cpp into theirDan Liew
2016-01-12[NFC] Refactor DummySolver out of Solver.cpp into its own fileDan Liew
2016-01-12[NFC] Refactor ValidatingSolver out of Solver.cpp into its own fileDan Liew
2016-01-07[NFC] Refactor SolverImpl out of Solver.cpp into its own fileDan Liew
2015-12-23Fix memory leak detected by ASan whenDan Liew
2015-12-23[NFC]Dan Liew
2015-12-18Move lib/Solver/SolverStats.h -> include/klee/SolverStats.hDan Liew
2015-12-17[Solver]Add support to dump STP qeries usingMartin Nowack
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 03:25:01 +0000