index
:
~cnx/klee
this commit
1.0.x
1.1.x
1.2.x
1.3.x
1.4.x
2.0.x
2.1.x
2.2.x
2.3.x
3.0.x
master
psychic
svcomp
svcomp_32bit
KLEE fork for patch differentiation testing
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
lib
/
Solver
Age
Commit message (
Expand
)
Author
2020-01-28
update
comet
2019-10-31
support compilation against LLVM 9.0
Julian Büning
2019-09-03
Moved solver-related header files into a separate klee/Solver/ directory.
Cristian Cadar
2019-09-03
Moved ConstructSolverChain.cpp to the Solver library.
Cristian Cadar
2019-09-03
Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated ...
Cristian Cadar
2019-07-30
Consolidated Expr-related include files into a single include/klee/Expr direc...
Cristian Cadar
2019-07-23
Refactor ConstraintManager to more modern coding standards
Daniel Schemmel
2019-07-23
Refactor ValueRange to more modern coding standards
Daniel Schemmel
2019-06-04
make endif guard naming consistent
Julian Büning
2019-06-04
make include guard naming consistent
Julian Büning
2019-06-04
Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ...
Cristian Cadar
2019-06-04
Remove parenthesis around returns, as reported and discussed in #891
Cristian Cadar
2019-03-20
STPSolver: C++11, add missing free, refactoring
Frank Busse
2019-03-13
Renamed --use-construct-hash to --use-construct-hash-stp and moved it and use...
Cristian Cadar
2019-03-13
Consistently use "default=true" and "default=false" instead of "default=on" a...
Cristian Cadar
2019-03-13
Added options in QueryLoggingSolver.cpp to the constraint solving category
Cristian Cadar
2019-03-13
Added options in CexCachingSolver.cpp to the constraint solving category and ...
Cristian Cadar
2019-03-11
Replaced "default=off" with "default=false"
MartinNowack
2019-03-11
Added options in STPSolver.cpp to the constraint solving category
Cristian Cadar
2019-03-11
Added Z3 options to the constraint solving category
Cristian Cadar
2019-01-15
make AssignmentLessThan::operator() const-invocable
Julian Büning
2018-10-30
Base time API upon std::chrono
Frank Busse
2018-10-23
refactor klee_open_output_file to return std::unique_ptr
Julian Büning
2018-10-23
use klee_open_output_file for uncompressed logs
Julian Büning
2018-10-16
Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ...
Cristian Cadar
2018-09-20
Silence an uninitialized variable compiler warning (and a tiny formatting cha...
Cristian Cadar
2018-07-04
Fix compiler warnings if assertions are disabled
Martin Nowack
2018-05-21
stop using DEBUG macro name
Jiri Slaby
2018-05-15
remove QueryLog.h
Frank Busse
2018-05-09
Improve handling of constant array in Z3
Timotej Kapus
2017-10-17
[cmake] detect available metaSMT backends using a pre-defined flag and raise ...
Hoang M. Le
2017-10-17
add support for CVC4 and Yices2 via metaSMT
Hoang M. Le
2017-10-04
Remove Autoconf/Makefile build system and adjust the TravisCI
Dan Liew
2017-07-08
Corrected comment of Z3Solver class
Andrew Santosa
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 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 the
Dan 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. This
Dan Liew
2017-06-01
[Z3] Move the `dump()` methods of the Z3NodeHandle<> specializations
Dan 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 going
Dan Liew
2017-05-24
llvm: make KLEE compile against LLVM 3.5 and 3.6
Richard Trembecký
2017-03-23
[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp
Dan Liew
2017-03-23
Add `AssignmentValidatingSolver`. It's purpose is to check any computed
Dan Liew
2017-03-03
Using klee_message instead of llvm:errs
Cristian Cadar
[next]