[dependabot]

Bumps z3-solver from 5.1.0.0 to 5.3.3.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit b3c1e0bacb804261488516043836258018ec0b7d

z3-5.3.3

5.3.3 release

z3-5.3.2

5.3.2 release

z3-5.3.1

5.3.1 release

z3-5.3.0

5.3.0 release

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

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

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

... (truncated)

Commits

• 430d19e Keep finite-set cardinality state consistent across backtracking (#11440)
• 68ba6f3 Integrate verified Java JARs into release artifacts (#11441)
• e171550 Fix unsound injectivity-axiom refinement when a passive bound variable repeat...
• 3e78041 Guard inverse-trigonometric rewrites by their domains (#11438)
• 5c15da4 Package Z3 Java API with bundled natives and layered CI (#11434)
• 70f966a F*: check integer rounding cuts in th-lemma arith unsupported steps (QF_LIA r...
• da5d957 Fix incremental symbolic Real-to-FP rounding with a linear encoding (#11421)
• b6cf396 Treat zero for the qi.profile_freq, branch_cut_ratio and horner_frequency opt...
• c95b61c Proof trimming: strip every negation so Boolean arguments trim (#11429)
• 5520d2f recfun_finder: do not move sibling conjuncts of an already guarded recursive ...
• 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)