Bump z3-solver from 5.0.0.0 to 5.1.0.0

[dependabot]

Bumps z3-solver from 5.0.0.0 to 5.1.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit 2f4a100b9a34ad4ffe076ded4b3534c76162f0ac

z3-5.1.0

5.1.0 release

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

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 5.2.0

Version 5.1.0

• New monadic regex solver enabled by default (smt.seq.regex_monadic=true). The solver uses live-state traversal and interval-refinement products for improved regex constraint solving, with semilinear length abstraction for regular expressions. Z3Prover/z3#10466, Z3Prover/z3#10472, Z3Prover/z3#10455, Z3Prover/z3#10389
• Add seq_monadic: configurable orientation (retry default) for reading regex memberships, light Antimirov cofactor mode, DNF replacement with depth-first search, and unsat-core extraction. Thanks to Margus Veanes. Z3Prover/z3#10519, Z3Prover/z3#10323, Z3Prover/z3#10366
• FPA rewriter simplifications for fma with zero multiplier. Fixes #8185. Thanks to Lev Nachmanson. Z3Prover/z3#9038
• LP-based nonlinear bound optimization for cross-nested conflicts; nonlinear bound optimization moved into monomial_bounds for improved NLA performance. Z3Prover/z3#10180, Z3Prover/z3#10434
• NLA: re-linearize violated monomials with fixed factors at final check; run bound squeeze before nonlinear engines and back off satisfiable nlsat probes. Thanks to Lev Nachmanson. Z3Prover/z3#10521
• Fix strict optimization objective reporting to preserve strict-real suprema in LRA path. Fixes #10534. Z3Prover/z3#10269
• Fix intblast soundness for array-derived BV equalities (smt.bv.solver=2). Z3Prover/z3#10485
• Fix str.at soundness inside regular expressions. Z3Prover/z3#10495
• Fix ill-sorted UF rewriting in fpa2bv for quantified Float32 arrays. Z3Prover/z3#10486
• Fix duplicate enode internalization for quantified Float32 datatype terms. Z3Prover/z3#10482
• Fix unsigned underflow of cardinality bounds in PB internalization. Z3Prover/z3#10515
• Fix assertion violation in lp_bound_propagator for columns with non-zero delta. Z3Prover/z3#10438
• Fix variable-divisor mod divisibility lemmas. Z3Prover/z3#10514
• Fix cached root index when negating algebraic numbers; reject rational values in algebraic root accessors. Z3Prover/z3#10530, Z3Prover/z3#10531
• Fix elim-term-ite simplifier soundness: add missing auxiliary variable constraints. Z3Prover/z3#10244
• Fix euf_arith_plugin missing uminus implementation. Z3Prover/z3#10243
• Fix QF_NRA: avoid degree-80 perfect-square factoring blowup by raising default prime trials.

... (truncated)

Commits

• 0b6cdcd Complete non-Rust medium-priority binding API coverage (#10537)
• c2a99f0 Update release notes for 5.1.0 (#10536)
• 74fb6c4 incrementing version to 5.1
• 9c70609 Fix incorrect strict optimization objective reporting (#10534)
• 12b0cd8 remove file that shouldn't be there
• f9c99af Remove hanging QF_NRA API test
• 221b77f fix #8185: add FPA rewriter simplifications for fma with zero multipl… (#9038)
• 3b0b5b3 Fix cached root index when negating algebraic numbers (#10530)
• 9228029 Reject rational values in algebraic root accessors (#10531)
• d9316f6 Change default regex_orientation to 'retry'
• 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)