about summary refs log tree commit diff homepage
path: root/lib/Solver/Z3Solver.cpp
AgeCommit message (Expand)Author
2024-01-30Change `GetConstraintLog` to work with `std::string`s instead of `char*`sDaniel Schemmel
2023-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in Z3SolverImplDaniel Schemmel
2023-03-23stats: rename numQueries/Queries -> SolverQueries, add QueriesFrank Busse
2022-08-26Use true instead of Z3_TRUE (removed in z3 4.11.0)Jerry James
2021-03-04[Z3] Handle the case when interruption caught by Z3Pavel Yatcheniy
2020-04-30Moved header files that were placed directly in include/klee/ into appropriat...Cristian Cadar
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-03-27Ensure that temp_builder is used when adding constant array value assertion c...Daniel Grumberg
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr direc...Cristian Cadar
2019-03-11Added Z3 options to the constraint solving categoryCristian Cadar
2018-10-30Base time API upon std::chronoFrank Busse
2018-10-23refactor klee_open_output_file to return std::unique_ptrJulian Büning
2018-09-20Silence an uninitialized variable compiler warning (and a tiny formatting cha...Cristian Cadar
2018-07-04Fix compiler warnings if assertions are disabledMartin Nowack
2018-05-09Improve handling of constant array in Z3Timotej Kapus
2017-06-02hide backend solver declarations from public includeHoang M. Le
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] Support another solver failure reason that Z3 might give. I'm goingDan Liew
2016-09-26Modified logging information to steer the usage of klee_message, klee_warning...Andrea Mattavelli
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
2016-02-14Add basic implementation of Z3Builder and Z3Solver and Z3SolverImplDan Liew