[dependabot]

Bumps z3-solver from 5.2.0 to 5.3.1.

Changelog

Sourced from z3-solver's changelog.

Version 5.3.1

• Fix unsound nonlinear-arithmetic exponentiation bounds: reverse exponent inequalities for bases below one and guard base-crossing refinements against negative exponents. Add F* counterexamples and soundness proofs for the corrected bounds. Fixes #11179. Z3Prover/z3@caa5da241
• Extend higher-order quantifier matching to nested Boolean connectives, array-store candidates, and arithmetic comparisons over array selections. Z3Prover/z3@30dd4fe48
• Extend Lean proof reconstruction to QF_UF and QF_LRA refutations from the legacy SMT proof object, including predicates whose arguments are all Boolean. Record arithmetic conflict and propagation coefficients for exact replay. Z3Prover/z3#11176
• Extend the F*/Pulse proof checker with unified, scoped proof-DAG checking, memoization, verified Boolean normalization and bounded truth-table rewrites, commutativity rules, and ground array theory-lemma checking. Keep unsupported steps as explicit unverified obligations. Z3Prover/z3@a1636cc9e, Z3Prover/z3@ee33c3f64, Z3Prover/z3@11306ced8
• Fix excessive Clang-CL warnings and compiler-warning flags leaking into Windows linker options. Avoid an unnecessary signed 128-bit division in finite-field inversion that caused static-link failures. Z3Prover/z3@1414db069
• Build Unix distribution binaries without embedded debug information to reduce archive size. Z3Prover/z3#11182

Version 5.3.0

This release contains substantial contributions:

• The build system is updated and consolidated to use CMake exclusively. Thanks to Alex Reinking

• It includes a first version of a Finite Field theory solver. Thanks to Romain Soulat.

• Add QF_FF (finite field) logic support, imported from the community branch RSoulatIOHK/z3:codex/qf-ff. Thanks to Romain Soulat. Z3Prover/z3#11019, Z3Prover/z3#11020

• Add a higher-order quantifier solver. Z3Prover/z3#10639

• Add associative and sequence EUF plugins. Z3Prover/z3#10752

• Add native Boolean proof certificates and Lean reconstruction for QF_LRA and QF_UF refutations, including Real and uninterpreted-sort ITE terms, multiple uninterpreted sorts, and Boolean arguments to uninterpreted functions. Outline long refutations into bounded Lean lemmas for scalable proof replay. Z3Prover/z3#11017, Z3Prover/z3#11085, Z3Prover/z3#11143, Z3Prover/z3#11144, Z3Prover/z3#11167, Z3Prover/z3#11168

... (truncated)

Commits

• See full diff 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)

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
typesafe-ai-playground	Ready	Preview	Oct 20, 2026 8:46am UTC

[dependabot]

Labels

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

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

[dependabot]

Superseded by #92.