[dependabot]

Bumps z3-solver from 5.1.0.0 to 5.3.2.0.

Release notes

Sourced from z3-solver's releases.

z3-5.3.3

5.3.3 release

Nightly

Automated nightly build from commit c95b61cb03b22e258dfbc5941262c9273e6650bd

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

• b411c90 Update 5.3.2 release notes for recent solver and tooling changes
• 871b1d0 [WIP] Fix regression in MBQI model finding from version 5.1.0 (#11320)
• 8d372e7 Fix unsound array equalities involving stores over lambdas (#11322)
• 85f45b6 Automate artifact-backed Pulse checker repair handoffs
• d81d8af Use the stored value for singleton array defaults in SAT SMT (#11324)
• 2203323 Count stores on both sides when expanding array equality (#11326)
• 1d790df Remove 'including OCaml' from CI status
• 8ce6f2b Preview generated Fstar models in audit PR comments
• 5c786f5 Consolidate OCaml binding checks into CI
• 871cad4 Split arithmetic proof obligations in standalone checkers
• Additional commits viewable in compare view

[dependabot]

Superseded by #43.