[Release Notes] Release notes for version 4.15.5

[github-actions[bot]]

This document contains formatted release notes ready to be added to RELEASE_NOTES.md for version 4.15.5.

Summary Statistics

• Date Range: October 29, 2025 to January 19, 2026
• Total Commits: 304
• Substantial Changes: 7 major items
• External Contributions: 1 (Ilana Shapiro)

Formatted Release Notes Content

The following content should be inserted into RELEASE_NOTES.md after the "Version 4.next" section and before the "Version 4.15.4" section:

Version 4.15.5
==============
- Add RCF (Real Closed Field) API to TypeScript bindings, achieving feature parity with Python, Java, C++, and C# implementations. 
  The API includes 38 functions for exact real arithmetic with support for π, e, algebraic roots, and infinitesimals.
  https://github.com/Z3Prover/z3/pull/8225
- Add sequence higher-order functions (map, fold) to Java, C#, and TypeScript APIs. Functions include SeqMap, SeqMapi, SeqFoldl, and SeqFoldli
  for functional programming patterns over sequences.
  - Java API: https://github.com/Z3Prover/z3/pull/8226
  - C# API: https://github.com/Z3Prover/z3/pull/8227
  - TypeScript API included in https://github.com/Z3Prover/z3/pull/8228
- Add benchmark export functionality to C# and TypeScript APIs for exporting solver problems as SMTLIB2 benchmarks.
  https://github.com/Z3Prover/z3/pull/8228
- Fix UNKNOWN bug in search tree with inconsistent end state during nonchronological backjumping. The fix ensures all node closing
  occurs in backtrack to maintain consistency between search tree and batch manager state. Thanks to Ilana Shapiro.
  https://github.com/Z3Prover/z3/pull/8214
- Fix segmentation fault in dioph_eq.cpp when processing UFNIRA problems without explicit set-logic declarations. Added bounds checks
  before accessing empty column vectors. https://github.com/Z3Prover/z3/pull/8218, fixes #8208
- Migrate build and release infrastructure from Azure Pipelines to GitHub Actions, including CI workflows, nightly builds, and release packaging.
- Bug fixes including #8195

Instructions for Maintainers

To apply these release notes to RELEASE_NOTES.md:

1. Open RELEASE_NOTES.md in your editor
2. Locate the "Version 4.next" section (should be near the top)
3. The empty "Version 4.15.5" section should already exist below it
4. Replace the empty "Version 4.15.5" section with the formatted content above
5. Ensure the "Version 4.next" section remains unchanged at the top
6. Commit the changes with message: "Update RELEASE_NOTES.md for version 4.15.5"

Notable Changes Excluded

The following types of changes were not included in the release notes as they are primarily internal or infrastructure improvements:

• C++20 modernization (range-based for loops, std::format)
• Workflow configuration improvements
• Build system tweaks
• Documentation updates
• Code cleanup and refactoring

Release Timeline

Version 4.15.4 was released on October 29, 2025. The commits for version 4.15.5 span from October 29, 2025 to January 19, 2026.

AI generated by Release Notes Updater