mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity
z3/src
History
Exact
Lev Nachmanson e83e8f695a
Fix array lambda final-check livelock (snapshot-regression iss-6364) 
Reverting the registration of lambda enodes with the legacy array
solver (added in 63259d8a4) that caused a non-terminating final-check
livelock on nested-array benchmarks such as inputs/issues/iss-6364/small-5.smt2,
which regressed from 'sat' to a timeout.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
2026-07-11 00:02:45 -07:00
..
ackermannization block ackermann over nested selects 2026-06-19 10:41:56 -07:00
api Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
ast remove ad-hoc disabling skolem shadowing in pattern inference 2026-07-10 14:25:20 -07:00
cmd_context fix pattern inference to deal with binders properly, pin sorts in tptp_frontend 2026-07-08 15:29:05 -07:00
math opt: validate strict optimization optima faithfully with delta-rational bounds (#10059) 2026-07-09 10:39:23 -07:00
model updates to tptp_frontend 2026-07-04 14:34:21 -07:00
muz Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
nlsat Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
opt opt: validate strict optimization optima faithfully with delta-rational bounds (#10059) 2026-07-09 10:39:23 -07:00
params change bit-vector AC simplification n to true 2026-07-10 15:00:32 -07:00
parsers Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
qe Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
sat Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
shell Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
smt Fix array lambda final-check livelock (snapshot-regression iss-6364) 2026-07-11 00:02:45 -07:00
solver Fix unsigned overflow in parallel solver conflict budget escalation (#10076) 2026-07-10 15:25:57 -07:00
tactic [snapshot-regression-fix] Fix elim_uncnstr disabled by manager-wide has_type_vars() flag (iss-6260/small-2) (#10063) 2026-07-07 13:02:37 -07:00
test bugfixes to front-end and matcher 2026-07-06 17:14:41 -07:00
util bug fixes to ho_matching - offset alignment inv_var_shift, callback scopes should not be nested, allow bindings that are not ground 2026-07-09 19:16:12 -07:00
CMakeLists.txt git bindings v1.0 2026-02-18 21:02:25 -08:00