Update z3-solver requirement from <=4.13.4.0,>=4.8.8.0 to >=4.8.8.0,<=4.15.7.0

[dependabot]

Updates the requirements on z3-solver to permit the latest version.

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 4.next

• Planned features
  • sat.euf
    • CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
  • add global incremental pre-processing for the legacy core.

Version 4.15.6

• Optimize mpz (multi-precision integer) implementation using pointer tagging to reduce memory footprint and improve performance. Z3Prover/z3#8447, thanks to Nuno Lopes.
• Fix macOS install_name_tool issue by adding -Wl,-headerpad_max_install_names linker flag to all dylib builds. Resolves "larger updated load commands do not fit" errors when modifying library install names on macOS. Z3Prover/z3#8535, fixes [#7623](https://github.com/Z3Prover/z3/issues/7623)
• Optimize parameter storage by storing rational values directly in variant instead of using pointers. Thanks to Nuno Lopes. Z3Prover/z3#8518

Version 4.15.5

• NLSAT now uses the Level wise algorithm for projection. https://arxiv.org/abs/2212.09309
• 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. Z3Prover/z3#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: Z3Prover/z3#8226
  • C# API: Z3Prover/z3#8227
  • TypeScript API included in Z3Prover/z3#8228
• Add benchmark export functionality to C# and TypeScript APIs for exporting solver problems as SMTLIB2 benchmarks. Z3Prover/z3#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. Z3Prover/z3#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. Z3Prover/z3#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
• Add functional datatype update operation to language bindings. The datatype_update_field function enables immutable updates to datatype fields, returning a modified copy while preserving the original datatype value. Z3Prover/z3#8500
• Add comprehensive regex support to TypeScript API with 21 functions including Re, Loop, Range, Union, Intersect, Complement, and character class operations. Enables pattern matching and regular expression constraints in TypeScript applications. Z3Prover/z3#8499
• Add move constructor and move assignment operator to z3::context class for efficient resource transfer. Enables move semantics for context objects while maintaining safety with explicit checks against moved-from usage. Z3Prover/z3#8508
• Add solve_for and import_model_converter functions to C++ solver API, achieving parity with Python API for LRA variable solving. Z3Prover/z3#8465

... (truncated)

Commits

• See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

[CLAassistant]

Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution.
_{You have signed the CLA already but the status is still pending? Let us recheck it.}

[dependabot]

Superseded by #1923.