[Release Notes] Release notes updates for version 4.15.5

[github-actions[bot]]

Release Notes Analysis for Version 4.15.5

Based on analysis of commits from z3-4.15.4 to HEAD (81 commits since Jan 18, 2026), the following substantial changes should be added to the existing Version 4.15.5 section in RELEASE_NOTES.md:

---

Formatted Content to Add

The following content should be appended to the existing Version 4.15.5 section (after the current entries):

- Add SLS (Stochastic Local Search) tactic as a separate worker thread for parallel solving of LIA problems. The SLS worker 
  can be enabled using the sls.threads parameter and runs independently of other workers, notifying the batch manager upon 
  finding solutions. Thanks to Ilana Shapiro. https://github.com/Z3Prover/z3/pull/8263
- Add Windows ARM64 Python wheel builds to nightly and release pipelines, enabling native Python bindings for Windows 
  on ARM64 architecture. https://github.com/Z3Prover/z3/pull/8280
- Fix solver state preservation with push/pop for multiple objectives. The fix ensures the initial state of the solver 
  is properly restored when using push/pop operations with multiple optimization objectives. Also fixes memory corruption 
  in Z3_polynomial_subresultants API function. https://github.com/Z3Prover/z3/pull/8264
- Fix missing newline after attributes in benchmark_to_smtlib_string that could produce invalid SMT-LIB output when 
  attributes don't end with a newline. Thanks to Josh Berdine. https://github.com/Z3Prover/z3/pull/8276
- Fix memory leak in linear programming solver's undo_fixed_column for big numbers. The fix explicitly resets mpq values 
  to free heap-allocated memory in region-allocated trail structures.

---

Summary

• 5 substantial changes documented
• 2 external contributions acknowledged (Ilana Shapiro, Josh Berdine)
• Date range analyzed: January 18-26, 2026
• Commits analyzed: 81 commits after the last documented PR in Version 4.15.5

Notes for Maintainers

1. The existing Version 4.15.5 section already contains 6 entries (RCF API, sequence functions, benchmark export, bug fixes, and migration to GitHub Actions)
2. These 5 new entries should be appended to the existing section
3. The Version 4.next section should remain unchanged at the top of the file
4. All entries follow the existing formatting style with bullet points, PR links, and proper attribution

Key Changes Highlighted

• New feature: SLS tactic as parallel worker (significant for performance on LIA problems)
• Platform support: Windows ARM64 wheels (expands platform compatibility)
• Important bug fixes:
  • Solver state preservation for optimization
  • Memory corruption in polynomial API
  • Memory leak in LP solver
  • SMT-LIB output formatting

The changes represent meaningful improvements to functionality, platform support, and reliability that users should be aware of.

AI generated by Release Notes Updater

• expires on Feb 3, 2026, 4:19 PM UTC