[Release Notes] Release notes for version 4.17.0 - Additional updates

[github-actions[bot]]

Release Notes Update for Version 4.17.0

The RELEASE_NOTES.md file was last updated on February 21, 2026. Since then, there have been 162 additional commits that should be documented for the 4.17.0 release.

Summary

• Date range analyzed: February 21, 2026 - March 2, 2026
• Total commits: 162
• Maintainer changes: Multiple bug fixes, API additions, and improvements
• External contributions: 3 notable contributions from the community

---

Formatted Content to Add to RELEASE_NOTES.md

The following content should be appended to the existing Version 4.17.0 section in RELEASE_NOTES.md:

- Add missing API methods across multiple language bindings for improved API completeness:
  - Python: BvNand, BvNor, BvXnor, Optimize.translate()
  - Go: MkAsArray, MkRecFuncDecl, AddRecDef, Model.Translate, tactic/simplifier functions, 8 BV overflow/underflow check functions
  - TypeScript: Array.fromFunc, Model.translate, comprehensive regex support with 21 functions, Optimize documentation improvements
  - OCaml: Model.translate
  - Java and C#: add_string, set_phase, get_units, get_non_units, get_levels methods
  https://github.com/Z3Prover/z3/pull/8793, https://github.com/Z3Prover/z3/pull/8813, https://github.com/Z3Prover/z3/pull/8824, https://github.com/Z3Prover/z3/pull/8825, https://github.com/Z3Prover/z3/pull/8758, https://github.com/Z3Prover/z3/pull/8781
- Add parser_context to C++ API for improved parsing functionality. Thanks to Toby Shi.
  https://github.com/Z3Prover/z3/pull/8722
- Add missing Java API method for as-array. Thanks to Ruijie Fang.
  https://github.com/Z3Prover/z3/pull/8762
- Expose mk_re_allchar in OCaml API for regular expression support. Thanks to Filipe Marques.
  https://github.com/Z3Prover/z3/pull/8785
- Implement register_on_clause callbacks for OCaml and TypeScript bindings.
  https://github.com/Z3Prover/z3/pull/8781
- Convert tactics to simplifiers for better composability:
  - bv1-blast tactic now available as simplifier
  - blast-term-ite tactic now available as simplifier
  https://github.com/Z3Prover/z3/pull/8779, https://github.com/Z3Prover/z3/pull/8780
- `Fix #7677`: treat FC_CONTINUE from check_nla as FEASIBLE in maximize for correct optimization behavior.
  https://github.com/Z3Prover/z3/pull/8801
- `Fix #7951`: add cancellation checks to polynomial gcd_prs and HNF computation to prevent hangs.
  https://github.com/Z3Prover/z3/pull/8801
- `Fix #7507`: simplify (>= product_of_consecutive_ints 0) to true for better arithmetic reasoning.
  https://github.com/Z3Prover/z3/pull/8789
- Fix assertion violation in q_mbi diagnostic output.
  https://github.com/Z3Prover/z3/pull/8805
- Fix memory leaks in model_based_opt def ref-counting.
  https://github.com/Z3Prover/z3/pull/8803
- Fix intblast ubv_to_int bug by adding bv2int axioms for compound expressions.
  https://github.com/Z3Prover/z3/pull/8767
- Fix TypeScript Array.fromFunc to use correct Z3_func_decl type handling.
  https://github.com/Z3Prover/z3/pull/8824
- Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, garbage values.
  https://github.com/Z3Prover/z3/pull/8824, https://github.com/Z3Prover/z3/pull/8766
- Handle overflow predicates in new core bit-vector internalization.
  https://github.com/Z3Prover/z3/pull/8801
- Optimize NLSAT levelwise algorithm parameter defaults (lws_subs_witness_disc, lws_spt_threshold). Thanks to Lev Nachmanson.
  https://github.com/Z3Prover/z3/pull/8770
- Bug fixes including issues reported by Maria Novoszel and multiple community members.

---

Instructions for Maintainers

To apply these updates to RELEASE_NOTES.md:

1. Open RELEASE_NOTES.md
2. Navigate to the Version 4.17.0 section (currently lines 4-24)
3. Append the formatted content above to the existing Version 4.17.0 entries (before the Version 4.16.0 section)
4. Ensure consistent formatting with bullet points using -
5. Verify all PR links are properly formatted
6. Do NOT modify the existing Version 4.17.0 content or the Version 4.16.0 section

Analysis Details

External Contributions (3):

1. Toby Shi - C++ parser_context API (Add parser_context in C++ API #8722)
2. Ruijie Fang - Java as-array method (Add missing Java API for as-array  #8762)
3. Filipe Marques - OCaml mk_re_allchar (Expose mk_re_allchar in OCaml API #8785)

Notable Changes:

• Multiple API completeness improvements across Python, Go, TypeScript, OCaml, Java, and C# bindings
• Three important bug fixes with issue numbers: Potential issue in arithmetic optimization #7677, Another seemingly infinite loop #7951, SAT check on an ite returning an unexpected unknown #7507
• Memory leak fixes and performance optimizations
• Tactic-to-simplifier conversions for better composability
• Static analysis issue fixes

Commit Statistics:

• Total: 162 commits analyzed
• Period: Feb 21, 2026 - Mar 2, 2026
• Maintainer commits: ~150 (including Nikolaj Bjorner, Lev Nachmanson)
• External contributor commits: 7
• Bot/automation commits: excluded from analysis

AI generated by Release Notes Updater

• expires on Mar 9, 2026, 8:45 PM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-09T20:45:51.789Z.

Closed by Workflow