From afe4bfcab29a232e7456eddcf8aa6ce697c538c7 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 20 Mar 2026 00:17:55 -0700 Subject: [PATCH] chore: update RELEASE_NOTES.md for 4.17.0 per discussion #9023 (#9051) 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 | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index f0fdb2543..d5d487c77 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -40,6 +40,26 @@ Version 4.17.0 - Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, and null pointer dereferences - Convert bv1-blast and blast-term-ite tactics to also expose as simplifiers for more flexible integration - Change default of param lws_subs_witness_disc to true for improved NLSAT performance. Thanks to Lev Nachmanson. +- Nl2Lin integrates a linear under-approximation of a CAD cell by Valentin Promies for improved NLSAT performance on nonlinear arithmetic problems. + https://github.com/Z3Prover/z3/pull/8982 +- Fix incorrect optimization of mod in box mode. Fixes #9012 +- Fix inconsistent optimization with scaled objectives in the LP optimizer when nonlinear constraints prevent exploration of the full feasible region. + https://github.com/Z3Prover/z3/pull/8998 +- Fix NLA optimization regression and improve LP restore_x handling. + https://github.com/Z3Prover/z3/pull/8944 +- Enable sum of monomials simplification in the optimizer for improved nonlinear arithmetic optimization. +- Convert injectivity and special-relations tactics to simplifier-based implementations for better integration with the simplifier pipeline. + https://github.com/Z3Prover/z3/pull/8954, https://github.com/Z3Prover/z3/pull/8955 +- Fix assertion violation in mpz.cpp when running with -tr:arith tracing. + https://github.com/Z3Prover/z3/pull/8945 +- Additional API improvements: + - Java: numeral extraction helpers (getInt, getLong, getDouble for ArithExpr and BitVecNum). Thanks to Angelica Moreira, https://github.com/Z3Prover/z3/pull/8978 + - Java: missing AST query methods (isTrue, isFalse, isNot, isOr, isAnd, isDistinct, getBoolValue, etc.). Thanks to Angelica Moreira, https://github.com/Z3Prover/z3/pull/8977 + - Go: Goal, FuncEntry, Model APIs; TypeScript: Seq higher-order operations (map, fold). https://github.com/Z3Prover/z3/pull/9006 +- Fix API coherence issues across Go, Java, C++, and TypeScript bindings. + 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 Version 4.16.0 ==============