Bump z3-solver from 4.15.4.0 to 4.16.0.0

[dependabot]

Bumps z3-solver from 4.15.4.0 to 4.16.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit 2c7b256db21f364cf37752e91cf750bf0b570f2c

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
• 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.
• Add ASan/UBSan memory safety CI workflow for continuous runtime safety checking. Thanks to Angelica Moreira. Z3Prover/z3#8856
• Add missing API bindings across multiple languages:
  • Python: BvNand, BvNor, BvXnor operations, Optimize.translate()
  • Go: MkAsArray, MkRecFuncDecl, AddRecDef, Model.Translate, MkBVRotateLeft, MkBVRotateRight, MkRepeat, and 8 BV overflow/underflow check functions
  • TypeScript: Array.fromFunc, Model.translate
  • OCaml: Model.translate, mk_re_allchar (thanks to Filipe Marques, Z3Prover/z3#8785)
  • Java: as-array method (thanks to Ruijie Fang, Z3Prover/z3#8762)
• Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
• Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation
• Fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize
• Fix assertion violation in q_mbi diagnostic output
• Fix memory leaks in model_based_opt def ref-counting
• Fix NoSuchFieldError in JNI for BoolPtr: use Z field descriptor and SetBooleanField
• Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type
• Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions
• Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, and null pointer dereferences
• Convert bv1-blast and blast-term-ite tactics to also expose as simplifiers for more flexible integration
• Change default of param lws_subs_witness_disc to true for improved NLSAT performance. Thanks to Lev Nachmanson.
• Nl2Lin integrates a linear under-approximation of a CAD cell by Valentin Promies for improved NLSAT performance on nonlinear arithmetic problems. Z3Prover/z3#8982
• Fix incorrect optimization of mod in box mode. Fixes #9012
• Fix inconsistent optimization with scaled objectives in the LP optimizer when nonlinear constraints prevent exploration of the full feasible region. Z3Prover/z3#8998
• Fix NLA optimization regression and improve LP restore_x handling. Z3Prover/z3#8944
• Enable sum of monomials simplification in the optimizer for improved nonlinear arithmetic optimization.

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