deps: Bump z3-solver from 4.16.0.0 to 5.0.0.0

[dependabot]

Bumps z3-solver from 4.16.0.0 to 5.0.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

Automated nightly build from commit b8c098f0017989076b1ebce9dded2a34a53cce11

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)
• 9a2867aeb7eaefadce0792a4f54f9387a5f66aa2 Add a fast-path to _coerce_exprs. (#7995)
• 06ed96dbda5ef3adc323ce2b4d3e5cfe13c1963a add the "noexcept" keyword to value_score=(value_score&&) declaration
• f2e7abbdc13182c3ba0898f8618659baaa50148a disable manylinux until segfault is resolved
• aaaa32b4a0644e6febf6336d1ae4a187ae28a911 build fixes
• d65c0fbcd650903b7a13cf7dd8a7fd92b8998410 add explicit constructors for nightly mac build failure
• fcc7e0216734bdac1a1f7f371c5d72343d95d08d Update arith_rewriter.cpp
• 62ee7ccf65d51c304553def478731aa17b848169 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985)
• 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80 Add finite_set_value_factory for creating finite set values in model generation (#7981)
• a1792861831973e6cfed98b955f59742b1065be3 restore the method behavior

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 5.0.0

• A FiniteSets theory solver FiniteSets is a theory with a sort (FiniteSet S) for base sort S. Inhabitants of (FiniteSet S) are finite sets of elements over S. The main operations are creating empty sets, singleton sets, union, intersection, set difference, ranges of integers, subset modulo a predicate. Constraints are: membership, subset. The size of a set is obtained using set.size. It is possible to map a function over elements of a set using set.map. Support for set.range, set.map is partial. Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s
• Add Python API convenience methods for improved usability. Thanks to Daniel Tang.
  • Solver.solutions(t) method for finding all solutions to constraints, Z3Prover/z3#8633
  • ArithRef.abs alias to integrate with Python's abs() builtin, Z3Prover/z3#8623
  • Improved error message in ModelRef.getitem to suggest using eval(), Z3Prover/z3#8626
  • Documentation example for Solver.sexpr(), Z3Prover/z3#8631
• Performance improvements by replacing unnecessary copy operations with std::move semantics for better efficiency. Thanks to Nuno Lopes, Z3Prover/z3#8583
• Fix spurious sort error with nested quantifiers in model finder. Fixes [#8563](https://github.com/Z3Prover/z3/issues/8563)
• NLSAT optimizations including improvements to handle_nullified_poly and levelwise algorithm. Thanks to Lev Nachmanson.
• Add ASan/UBSan memory safety CI workflow for continuous runtime safety checking. Thanks to Angelica Moreira. Z3Prover/z3#8856
• Add missing API bindings across multiple languages:
  • Python: BvNand, BvNor, BvXnor operations, Optimize.translate()
  • Go: MkAsArray, MkRecFuncDecl, AddRecDef, Model.Translate, MkBVRotateLeft, MkBVRotateRight, MkRepeat, and 8 BV overflow/underflow check functions
  • TypeScript: Array.fromFunc, Model.translate
  • OCaml: Model.translate, mk_re_allchar (thanks to Filipe Marques, Z3Prover/z3#8785)
  • Java: as-array method (thanks to Ruijie Fang, Z3Prover/z3#8762)
• Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
• Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation
• Fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize
• Fix assertion violation in q_mbi diagnostic output
• Fix memory leaks in model_based_opt def ref-counting
• Fix NoSuchFieldError in JNI for BoolPtr: use Z field descriptor and SetBooleanField
• Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type
• Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions
• Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, and null pointer dereferences
• Convert bv1-blast and blast-term-ite tactics to also expose as simplifiers for more flexible integration
• Change default of param lws_subs_witness_disc to true for improved NLSAT performance. Thanks to Lev Nachmanson.
• Nl2Lin integrates a linear under-approximation of a CAD cell by Valentin Promies for improved NLSAT performance on nonlinear arithmetic problems. Z3Prover/z3#8982
• Fix incorrect optimization of mod in box mode. Fixes #9012
• Fix inconsistent optimization with scaled objectives in the LP optimizer when nonlinear constraints prevent exploration of the full feasible region. Z3Prover/z3#8998
• Fix NLA optimization regression and improve LP restore_x handling. Z3Prover/z3#8944
• Enable sum of monomials simplification in the optimizer for improved nonlinear arithmetic optimization.

... (truncated)

Commits

• 8e3402b wasm: pin Node.js to v22 instead of lts/* to avoid manifest fetch failures (#...
• d722fb1 update release notes
• 7ba8861 update version
• 3751bfa Bump actions/cache/save from 5.0.5 to 6.1.0 (#10149)
• b39692a Bump actions/setup-dotnet from 5 to 6 (#10147)
• 0739cd2 Bump actions/checkout from 6.0.2 to 7.0.0 (#10146)
• bb9dc5e Bump actions/setup-node from 6 to 7 (#10148)
• 7e29ea7 Bump actions/setup-go from 6 to 7 (#10150)
• 63730fe Fix swapped assert_expr arguments in smt_solver::translate for named assertio...
• 2a3b64a fix #10137
• Additional commits viewable in compare view

[aallan]

@dependabot rebase

[aallan]

Holding this one for about a week — not because anything failed, but because the evidence doesn't yet cover the risk.

What was checked

A per-obligation differential between 4.16.0.0 and 5.0.0.0 across all 39 examples and all 163 conformance programs — comparing each obligation's kind, status, source line, column and description, not just the summary counts:

• 2,329 obligations, byte-identical between the two versions
• Zero tier3 → verified transitions, so 5.0.0 proves nothing 4.16.0 didn't — which also rules out the soundness direction of a solver regression
• Full suite green on 5.0.0 (8,167 passed), 163 conformance, 39 examples
• test_rounding_relation_not_proved (the Z3-budget-sensitive one behind test_rounding_relation_not_proved asserts stricter than its docstring — spurious failure when Z3 falls to Tier 3 #1121) stable at 0.93s across five runs — no timing drift

Why that isn't enough here

That differential proves identical behaviour on the paths this corpus reaches. The risk in this particular bump lives in the paths it doesn't:

5.0.0 published	2026-07-17 — four days ago
Release notes	13 characters, no documented changes
Commits since 4.16.0	1,699

A major version with 1,699 commits, no published changelog, and four days of field exposure — in the verification core of a language whose whole premise is proof. #996 is already on the books as a conformance flake that surfaced once in ~960 runs, which is exactly the shape of defect 2,329 obligations would not catch.

Nothing in Vera needs a 5.0 feature, so there is no cost to waiting.

Plan

Revisit in a week or so and re-run the same differential — the capture scripts are kept, so it is a ten-minute check. If it is still identical and 5.0.0 has had some field exposure by then, it goes in.

Leaving this PR open rather than closing it; no need for @dependabot to recreate it in the meantime.

[aallan]

Tracked as #1126, which carries the reasoning, the exact re-check script and the merge criteria — so the decision survives independently of this PR thread.

Handling until then: keep this PR rebased as main moves (@dependabot rebase, not recreate — a recreate can re-resolve to a different version and silently invalidate the differential, whose whole value is that a specific version was measured). Revisit from 2026-07-28.

[aallan]

@dependabot rebase

[aallan]

@dependabot rebase

[aallan]

@dependabot rebase

[dependabot]

Looks like this PR is already up-to-date with main! If you'd still like to recreate it from scratch, overwriting any edits, you can request @dependabot recreate.

[aallan]

@dependabot rebase

[aallan]

Tracked in #1126. Holding until 5.0.0.0 bakes in.