From cf051598f979a2d781c2851008c54baf670c04f2 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 1 Apr 2026 08:54:45 -0700 Subject: [PATCH] Update RELEASE_NOTES.md with Version 4.17.0 additions from discussion #9172 (#9186) Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/488739ce-e615-410e-8956-677db4c0df2a Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- RELEASE_NOTES.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index d5d487c77..2e44bbe56 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -60,6 +60,37 @@ Version 4.17.0 https://github.com/Z3Prover/z3/pull/8983 - Fix deep API bugs in Z3 C API (null pointer handling, error propagation). https://github.com/Z3Prover/z3/pull/8972 +- Implement multivariate polynomial factorization via Hensel lifting. Replaces the prior stub + implementation (factor_n_sqf_pp) with a working algorithm: evaluate away extra variables to + reduce to bivariate, factor the univariate specialization, lift via linear Hensel lifting in + Zp[x], and verify the result over Z[x,y]. For more than two variables, bivariate factors are + checked against the original polynomial. Thanks to Lev Nachmanson. +- Add riscv64 Python wheel builds to nightly and release PyPI publishing. + https://github.com/Z3Prover/z3/pull/9153 +- Fix nlsat clear() crash: reset polynomial cache and root-atom assignments during solver + destruction to prevent use-after-free heap corruption. Also fix scoped_numeral_vector copy + constructor to read from the source operand instead of uninitialized self. + https://github.com/Z3Prover/z3/pull/9150 +- Fix #9030: in box mode optimization (opt.priority=box), each objective is now optimized + independently using push/pop scopes, so adding or removing one objective no longer changes + the optimal values of others. +- Fix assertion violation in isolate_roots for nested nlsat calls. Fixes #6871. +- Fix #9036: expand bounded integer quantifiers in qe-light when Fourier-Motzkin elimination + fails due to non-unit coefficients. When all remaining quantified integers have explicit + finite bounds and the product of domain sizes is at most 10000, the quantifier is unrolled + into an explicit disjunction. +- Fix #8023: only skip adding an axiom clause when its satisfying literal is assigned at base + level (scope 0). The previous optimization was unsound: literals can be retracted by + backtracking, causing the string solver to miss propagations such as indexof(a,s) = -1 when + contains(a,s) becomes false after backtracking. +- Fix lock contention in theory_diff_logic and theory_dense_diff_logic when using multi-threaded + solving (smt.threads > 1). A diagnostic IF_VERBOSE(0,...) call was always acquiring the global + verbose mutex, causing catastrophic contention when multiple threads internalized atoms. + Fixes #8019. +- Fix string solver: move m_fixed insertion after check_long_strings guard to prevent premature + marking of string variables with length > 20 as processed. +- Fix documentation for Z3_solver_to_dimacs_string: corrected the function name in the API + comment. Thanks to Mark DenHoed, https://github.com/Z3Prover/z3/pull/9053 Version 4.16.0 ==============