[dependabot]

Bumps z3-solver from 5.1.0.0 to 5.3.1.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit ac62f5a6af3bd1b6805741264cbc02182db92239

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

• 887ecc0c98345533ab1ba28003d4e79fefd351c5 throttle grobner method more actively
• 58e64ea8264b42feb5a9c824bd4f3944aed65616 try exponential delay in grobner
• 2bf1cc7d61b3cd967791d7fdbb9790dd97e238e7 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988)
• 68a7d1e1b1cbca5796e0cbf647d6a940b08b4cde Bump actions/setup-node from 5 to 6 (#7994)

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 5.3.1

• Add native Complex arithmetic with (complex.make re im), (complex.real z), (complex.imag z), overloaded +, -, *, /, and equality. Simplification reduces complex arithmetic to pairs of Reals, supported by the default arithmetic solver, SAT/EUF arithmetic, and qfnra-nlsat. Division computes ((ac+bd)/(c*c+d*d), (bc-ad)/(c*c+d*d)) for (a+bi)/(c+di), using totalized Real division, including at zero. Complex numbers have no ordering. C, C++, .NET, Java, OCaml, JavaScript/TypeScript, and Python APIs expose the sort, constructor, projections, arithmetic, and typed model values.
• 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.

... (truncated)

Commits

• ac9156f Update release notes for version 5.3.1
• 76a825d Build Unix distribution binaries without debug information (#11182)
• e308968 Set version to 5.3.1
• caa5da2 Fix exponentiation bounds with F* soundness audit
• 59ca092 bump version
• 916ff9f Certify QF_UF, QF_LRA, and Bool-only predicate refutations from the legacy pr...
• 11306ce Prove SMT array axioms and check array theory lemmas
• ee33c3f Add verified rewrite rules and memoized proof DAG checking
• 1414db0 Fix Clang-CL warnings and static finite-field linking
• 6b40416 Merge remote master updates
• 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)

[dependabot]

Labels

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

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