about summary refs log tree commit diff homepage
path: root/lib
AgeCommit message (Expand)Author
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-10rename the configure option --with-metasmt-default-solver to --with-metasmt-d...Hoang M. Le
2016-06-10use default metaSMT solver as defined in configurationHoang M. Le
2016-06-10update Makefile for metaSMTHoang M. Le
2016-06-10clean up metaSMT includesHoang M. Le
2016-05-27Merge pull request #396 from andreamattavelli/fix_kleaver_parserCristian Cadar
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
2016-05-24Fixed bug #375 in Kleaver's parserAndrea Mattavelli
2016-05-18Modified -debug-print-instructions to allow to write directly on log file.Andrea Mattavelli
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-14Disabling --solver-optimize-divides by default, as the optimization is curren...Cristian Cadar
2016-04-12Merge pull request #364 from MartinNowack/feat_partial_loggingCristian Cadar
2016-04-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
2016-04-08Remove computation of ``isLocal`` that is always true when handlingDan Liew
2016-04-08Rename KLEE command line options fromDan Liew
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-22ExprPPrinter: Print out arrays deterministicallyMartin Nowack
2016-03-22Try to fix #348Dan Liew
2016-03-16push_back usage for values vectorvpushkar
2016-03-16Wrong std::vector 'values' usage after vector's capacity reserve. It is the e...vpushkar
2016-03-01Documented default values for various options and improved the description of...Cristian Cadar
2016-02-29Merge pull request #344 from MartinNowack/feat_mallocMartinNowack
2016-02-27Merge pull request #342 from delcypher/expr_fixesMartinNowack
2016-02-27Use klee-provided GetMallocUsage for consistencyMartin Nowack
2016-02-27Refactoring: Extract checking memory limit into own functionMartin Nowack
2016-02-27Add support for tcmallocMartin Nowack
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-23When calling ``Assignment::dump()`` if there are no bindings emitDan Liew
2016-02-23Move ``Assignment::dump()`` into its own implementation file soDan Liew
2016-02-22Remove stray STP function declaration.Dan Liew
2016-02-22Move Array constructor out of ``Expr.h`` and into ``Expr.cpp``.Dan Liew
2016-02-20Fix valueIsOnlyCalled() used by MD2U.Sean Bartell
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-02-08Fixed two spelling errors.Marko Dimjašević
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-21 08:22:03 +0000