mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-14 17:19:59 +00:00
Code Activity

Update RELEASE_NOTES.md with additional Version 4.17.0 entries from discussion #8907

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 18:39:34 +00:00
parent 240453e452
commit 175a50330b
1 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

19
RELEASE_NOTES.md
View file

@ -21,6 +21,25 @@ Version 4.17.0
Thanks to Nuno Lopes, https://github.com/Z3Prover/z3/pull/8583
- Fix spurious sort error with nested quantifiers in model finder. `Fixes #8563`
- NLSAT optimizations including improvements to handle_nullified_poly and levelwise algorithm. Thanks to Lev Nachmanson.
- Add ASan/UBSan memory safety CI workflow for continuous runtime safety checking. Thanks to Angelica Moreira.
https://github.com/Z3Prover/z3/pull/8856
- Add missing API bindings across multiple languages:
- Python: BvNand, BvNor, BvXnor operations, Optimize.translate()
- Go: MkAsArray, MkRecFuncDecl, AddRecDef, Model.Translate, MkBVRotateLeft, MkBVRotateRight, MkRepeat, and 8 BV overflow/underflow check functions
- TypeScript: Array.fromFunc, Model.translate
- OCaml: Model.translate, mk_re_allchar (thanks to Filipe Marques, https://github.com/Z3Prover/z3/pull/8785)
- Java: as-array method (thanks to Ruijie Fang, https://github.com/Z3Prover/z3/pull/8762)
- Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
- Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation
- Fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize
- Fix assertion violation in q_mbi diagnostic output
- Fix memory leaks in model_based_opt def ref-counting
- Fix NoSuchFieldError in JNI for BoolPtr: use Z field descriptor and SetBooleanField
- Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type
- Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions
- 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.
Version 4.16.0
==============