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

[dependabot]

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

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 4.17.0

• A FiniteSets theory solver FiniteSets is a theory with a sort (FiniteSet S) for base sort S. Inhabitants of (FiniteSet S) are finite sets of elements over S. The main operations are creating empty sets, singleton sets, union, intersection, set difference, ranges of integers, subset modulo a predicate. Constraints are: membership, subset. The size of a set is obtained using set.size. It is possible to map a function over elements of a set using set.map. Support for set.range, set.map is partial. Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s
• Add Python API convenience methods for improved usability. Thanks to Daniel Tang.
  • Solver.solutions(t) method for finding all solutions to constraints, Z3Prover/z3#8633
  • ArithRef.abs alias to integrate with Python's abs() builtin, Z3Prover/z3#8623
  • Improved error message in ModelRef.getitem to suggest using eval(), Z3Prover/z3#8626
  • Documentation example for Solver.sexpr(), Z3Prover/z3#8631
• Performance improvements by replacing unnecessary copy operations with std::move semantics for better efficiency. Thanks to Nuno Lopes, Z3Prover/z3#8583
• Fix spurious sort error with nested quantifiers in model finder. Fixes [#8563](https://github.com/Z3Prover/z3/issues/8563)
• NLSAT optimizations including improvements to handle_nullified_poly and levelwise algorithm. Thanks to Lev Nachmanson.

Version 4.16.0

• Add Go bindings to supported APIs

Version 4.15.8

• Fix release pipeline to publish all supported python wheels properly.
• Re-enable npm tokens for publishing npm pacages.

Version 4.15.7

• Bug fix release

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

... (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.}