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

[dependabot]

Bumps z3-solver from 4.16.0.0 to 5.0.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit 8e3402b215a810a4154eb183a7dfc4e853eb2f52

z3-5.0.0

5.0.0 release

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

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 5.0.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

• 8e3402b wasm: pin Node.js to v22 instead of lts/* to avoid manifest fetch failures (#...
• d722fb1 update release notes
• 7ba8861 update version
• 3751bfa Bump actions/cache/save from 5.0.5 to 6.1.0 (#10149)
• b39692a Bump actions/setup-dotnet from 5 to 6 (#10147)
• 0739cd2 Bump actions/checkout from 6.0.2 to 7.0.0 (#10146)
• bb9dc5e Bump actions/setup-node from 6 to 7 (#10148)
• 7e29ea7 Bump actions/setup-go from 6 to 7 (#10150)
• 63730fe Fix swapped assert_expr arguments in smt_solver::translate for named assertio...
• 2a3b64a fix #10137
• Additional commits viewable in compare view

[dependabot]

Labels

The following labels could not be found: python. Please create it before Dependabot can add it to a pull request.

Please fix the above issues or remove invalid values from dependabot.yml.