chore(deps): bump z3-solver from 4.15.8.0 to 4.16.0.0

[dependabot]

Bumps z3-solver from 4.15.8.0 to 4.16.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit ca1865c3fe51a68c84cdc0c169df096360c72ecc

z3-4.16.0

4.16.0 release

z3-4.15.8

4.15.8 release

z3-4.15.7

4.15.7 release

z3-4.15.6

4.15.6 release

z3-4.15.5

4.15.5 release

z3-4.15.4

Changes:

• 745087e237e669d709ae35694728a0c479e572b3 update release notes
• c88295a7c76cc62cf5a994c53d39766cc479abec fix C++ example and add polymorphic interface for C++
• 6efffa00548043d984b5e664d6076e40dac201a3 renemable Centos AMD nightly
• 1b9a6369107f6dd8ec2070f0edf9d90b45aa3ba0 fix build break introduced when adding support for polymorphic datatypes
• 88fcc05d6c17155a61517928ba6797f91e507de9 Bump actions/upload-artifact from 4 to 5 (#7998)
• 488c712f5b9891198542ccbfd02657964ed91cd0 Bump actions/download-artifact from 5 to 6 (#7999)
• 3570073c29382ef9ab8b1abc46622155edc631d2 Add missing mkLastIndexOf method and CharSort case to Java API (#8002)
• b6e3a688390be425713d96ef41c9de0ac83dfbc4 update centos version
• 766eaa3376ae53fe451148590cc3d50f6f6381be disable centos build until resolved
• efd5d04af50b5dc0a2203f59bb5b159101a964f1 enable always add all coeffs in nlsat

• 887ecc0c98345533ab1ba28003d4e79fefd351c5 throttle grobner method more actively
• 58e64ea8264b42feb5a9c824bd4f3944aed65616 try exponential delay in grobner
• 2bf1cc7d61b3cd967791d7fdbb9790dd97e238e7 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
• 68a7d1e1b1cbca5796e0cbf647d6a940b08b4cde Bump actions/setup-node from 5 to 6 (#7994)
• 9a2867aeb7eaefadce0792a4f54f9387a5f66aa2 Add a fast-path to _coerce_exprs. (#7995)
• 06ed96dbda5ef3adc323ce2b4d3e5cfe13c1963a add the "noexcept" keyword to value_score=(value_score&&) declaration
• f2e7abbdc13182c3ba0898f8618659baaa50148a disable manylinux until segfault is resolved
• aaaa32b4a0644e6febf6336d1ae4a187ae28a911 build fixes
• d65c0fbcd650903b7a13cf7dd8a7fd92b8998410 add explicit constructors for nightly mac build failure
• fcc7e0216734bdac1a1f7f371c5d72343d95d08d Update arith_rewriter.cpp
• 62ee7ccf65d51c304553def478731aa17b848169 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)
• 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80 Add finite_set_value_factory for creating finite set values in model generation (#7981)
• a1792861831973e6cfed98b955f59742b1065be3 restore the method behavior
• 1921260c424036b40f4fad1eb9a3f171590cdfd3 restore single cell
• 3b565bb2846f69bf1b3ae5eff297b0771d003892 trim parametric datatype test
• 5163411f9b90a339167a41fb3d46a4811420a4db Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966)

... (truncated)

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

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
• 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.

... (truncated)

Commits

• ddb4956 Merge pull request #8683 from Z3Prover/copilot/fix-build-error-z3
• 366b197 Fix OCaml build error in solver_get_levels
• b384f74 Initial plan
• 02b6aeb Merge pull request #8681 from Z3Prover/copilot/fix-discussion-issues-8680
• 6c02a3b Delete examples/go/test_new_api_additions.go
• 9d3cc4a remove deprecated workflows
• 672d243 Merge pull request #8682 from Z3Prover/copilot/fix-docs-and-update-script
• 9499b10 Add --go flag to mk_api_doc.py calls and remove go directory overwrite code
• 4335b9f Initial plan
• c74acb5 Add test for new Go API methods
• Additional commits viewable 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)

[codacy-production]

Coverage summary from Codacy

See diff coverage on Codacy

Coverage variation	Diff coverage
✅ +0.00% (target: -1.00%)	✅ ∅

Coverage variation details

	Coverable lines	Covered lines	Coverage
Common ancestor commit (a14f07e)	228	227	99.56%
Head commit (0b58e4a)	228 (+0)	227 (+0)	99.56% (+0.00%)

Coverage variation is the difference between the coverage for the head and common ancestor commits of the pull request branch: <coverage of head commit> - <coverage of common ancestor commit>

Diff coverage details

	Coverable lines	Covered lines	Diff coverage
Pull request (#60)	0	0	∅ (not applicable)

Diff coverage is the percentage of lines that are covered by tests out of the coverable lines that the pull request added or modified: <covered lines added or modified>/<coverable lines added or modified> * 100%

See your quality gate settings    Change summary preferences

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 98.92%. Comparing base (a14f07e) to head (0b58e4a).
⚠️ Report is 1 commits behind head on master.

Additional details and impacted files

@@           Coverage Diff           @@
##           master      #60   +/-   ##
=======================================
  Coverage   98.92%   98.92%           
=======================================
  Files           5        5           
  Lines         186      186           
  Branches       38       38           
=======================================
  Hits          184      184           
  Misses          1        1           
  Partials        1        1           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[vil02]

@dependabot recreate

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud