[dependabot]

Bumps z3-solver from 5.2.0 to 5.3.3.

Changelog

Sourced from z3-solver's changelog.

Version 5.3.3

• Java release packages: add API-only, platform-specific, and universal JARs to GitHub release artifacts. Bundled-native packages cover Linux x64, Windows x64, and macOS arm64; the universal JAR contains all three. Fall back to extracting and loading the bundled Z3 and JNI libraries when conventional native-library loading fails. Preserve z3.skipLibraryLoad and Java 8 compatibility. Gate release publication on source/version consistency, checksums, and native smoke tests; include provenance and validation reports. This does not add Maven publishing. Z3Prover/z3#11434, Z3Prover/z3#11441
• MaxSMT performance: bound core-guided optimization using the linear relaxation of hard constraints, and try integral soft-literal assignments from the relaxation before extracting cores. This improves problems with cardinality, pseudo-Boolean, and linear arithmetic constraints. Enable by default with opt.maxres.lp_relaxation, with a separate opt.maxres.lp_relaxation_rlimit budget. Thanks to Lev Nachmanson. Z3Prover/z3#11428
• Simplify modular inverse equalities over compound arithmetic expressions, including distributed sums and constant offsets, using bounded, coefficient-reducing rewrites. Z3Prover/z3#11365
• Fix incorrect transcendental results by validating actual witness intervals before widening enclosures and linking transcendental variables to their expanded polynomial definitions. Guard inverse-trigonometric and inverse-hyperbolic cancellation rewrites by their valid domains. Z3Prover/z3#11364, Z3Prover/z3#11438
• Fix incremental symbolic Real-to-floating-point rounding using a direct linear-real encoding that preserves all five rounding modes, signed zero, subnormals, ties, and overflow. Preserve NaN congruence across raw-bit constructors, uninterpreted functions, and array boundaries without restricting legal NaN signs or payloads. Z3Prover/z3#11421, Z3Prover/z3#11419
• Correct signed bit-vector modulus in integer blasting and avoid unsound folding of nested symbolic rotations at non-power-of-two widths. Z3Prover/z3#11417
• Resolve datatype match constructors using the scrutinee's instantiated sort. Detect recursive datatype cycles through sequence concatenations and equivalence classes, and correct subterm polarity, conflict dependencies, relevance, and antisymmetry. Reject unsupported nested recursion in :subterm declarations instead of producing incorrect results. Z3Prover/z3#11418, Z3Prover/z3#11411
• Preserve singleton cardinalities for datatype array fields with singleton ranges, including arrays over infinite index domains. Thanks to Roberto Pettinau. Z3Prover/z3#11330
• Keep finite-set cardinality completion state consistent with its Boolean subsolver across backtracking, preventing spurious zero-cardinality equations and incorrect unsat results.

... (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	Nov 3, 2026 8:45am 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.