mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-23 04:49:11 +00:00
Code Activity

chore: update RELEASE_NOTES.md for 4.17.0 per discussion #9023 (#9051)

Browse source 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-03-20 00:17:55 -07:00 • committed by GitHub
parent 1137d23725
commit afe4bfcab2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 20 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
RELEASE_NOTES.md
View file

@ -40,6 +40,26 @@ Version 4.17.0
- Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, and null pointer dereferences - 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 - 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. - 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 Version 4.16.0
============== ==============