Skip to content

build(deps): bump z3-solver in /packages/python-ta-z3 - #1392

Open
dependabot[bot] wants to merge 1 commit into
masterfrom
dependabot/uv/packages/python-ta-z3/uv-d89701adf2
Open

dependabot[bot] wants to merge 1 commit into
masterfrom
dependabot/uv/packages/python-ta-z3/uv-d89701adf2

Conversation

@dependabot

@dependabot dependabot Bot commented on behalf of github Sep 20, 2026

Copy link
Copy Markdown
Contributor

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

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

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 <dependency name> major version will close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)
  • @dependabot ignore <dependency name> minor version will close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)
  • @dependabot ignore <dependency name> will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)
  • @dependabot unignore <dependency name> will remove all of the ignore conditions of the specified dependency
  • @dependabot unignore <dependency name> <ignore condition> will remove the ignore condition of the specified dependency and ignore conditions

Updates the requirements on [z3-solver](https://github.com/Z3Prover/z3) to permit the latest version.

Updates `z3-solver` to 5.1.0.0
- [Release notes](https://github.com/Z3Prover/z3/releases)
- [Changelog](https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES.md)
- [Commits](https://github.com/Z3Prover/z3/commits/z3-5.1.0)

---
updated-dependencies:
- dependency-name: z3-solver
  dependency-version: 5.1.0.0
  dependency-type: direct:production
  dependency-group: uv
...

Signed-off-by: dependabot[bot] <support@github.com>
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file python:uv Pull requests that update python:uv code labels Sep 20, 2026
@coveralls

Copy link
Copy Markdown
Collaborator

Coverage Report for CI Build 35538782475

Coverage remained the same at 90.878%

Details

  • Coverage remained the same as the base build.
  • Patch coverage: No coverable lines changed in this PR.
  • No coverage regressions found.

Uncovered Changes

No uncovered changes found.

Coverage Regressions

No coverage regressions found.


Coverage Stats

Coverage Status
Relevant Lines: 4089
Covered Lines: 3716
Line Coverage: 90.88%
Coverage Strength: 17.66 hits per line

💛 - Coveralls

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

dependencies Pull requests that update a dependency file python:uv Pull requests that update python:uv code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant