3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
z3/src
Nikolaj Bjorner 7151c5ac6e fixes to finite domain arrays
- relevancy could be off and array solver doesn't compensate, #7544
- enforce equalities across store for small domain axioms #8065
2026-02-18 20:57:03 -08:00
..
ackermannization Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
api set build be configurable by env 2026-02-18 20:57:02 -08:00
ast fix #8097 2026-02-18 20:57:02 -08:00
cmd_context allow parsing declared arrays without requiring explicit select 2026-02-18 20:56:57 -08:00
math fix #8099 (again) 2026-02-18 20:57:03 -08:00
model Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) 2026-02-18 20:55:23 -08:00
muz fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables 2025-09-30 15:58:48 -07:00
nlsat remove unused *_signed_project() methods 2026-02-18 20:56:57 -08:00
opt fix #8076 2026-02-18 20:57:03 -08:00
params Some changes to improve LIA performance (#8101) 2026-02-18 20:57:03 -08:00
parsers patch definitions, add pretty print support 2025-10-13 22:39:32 +02:00
qe remove unused *_signed_project() methods 2026-02-18 20:56:57 -08:00
sat remove stale experimental code #8063 2026-02-18 20:56:58 -08:00
shell move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt fixes to finite domain arrays 2026-02-18 20:57:03 -08:00
solver include FS logic 2025-11-21 13:14:53 -08:00
tactic remove model converter operator on expr_ref& 2025-09-07 16:42:20 -07:00
test Fix DEL character (0x7F) not being escaped in string literals (#8080) 2026-02-18 20:56:59 -08:00
util Fix DEL character (0x7F) not being escaped in string literals (#8080) 2026-02-18 20:56:59 -08:00
CMakeLists.txt BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 2026-02-18 20:57:00 -08:00