chore(deps): bump z3-solver from 4.13.0.0 to 4.13.2.0

[dependabot]

Bumps z3-solver from 4.13.0.0 to 4.13.2.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

• 77aa5280dfd4960f615e98b669ff411c774598c5 wasm: increase timeout in tests (#7401)
• 103c5ad71c4526bfc0b7580bce3383940f953c8f wasm: attempt to GC in tests (#7400)
• 82eb18674b446f3a90992fc57cbb690ccd4cfa08 remove ubuntu build 20 from nightly
• eb5d036786d1c1571067f656ef9c42afa4a828b7 fix #7392
• 2655301afcdab4d98f2844f0a69d8ca2ff7aba38 comment out simple proofs unit test
• 8b81bda46959e82c7e333f5838f4a424f4289f92 Julia now used the C API. (#7388)
• 994056f347a637bfe90b224d4ffdeb2fde43b469 C API now used by Julia. (#7387)
• 716a815ce169492837f95bb7613f8ff6cb183b98 update lock file
• a831fe9609488a98ac53fba725bb54707ae27942 fix some build warnings
• afaa48d72af0bfad47a3b3b4cf745c3a6f7f1714 sample fix script

• fa1a2cdc1e5e808c59f6f70647eef4415e405bd5 disable simple check in nlsat
• c34c8477f3d10444f8142e6917a752f06af1e246 Add .gitattributes for genaiscript and update git commit flow script. (#7396)
• ec14ef765e20a1280d956c57458d3bda52e6ff5b Update Ubuntu job name in Azure pipeline and add string variable creation in C API example
• 95d2e009ef93fbcd07d531fc4360249a0afc13fa Update OCaml jobs to use Ubuntu-latest in Azure Pipelines configuration
• 0604d23c570970155ed56d58f545b8533d336be1 Check if model_converter is non-null before initializing values in sat_tactic
• 5a6dc18d0d7843a6b8583be193056fee467995f6 Override convert_initialize_value method in bit_blaster_model_converter.cpp
• 5c583299f1983bcd7300f82d96b1b81e5634baee Remove unnecessary const qualifiers from comparison operator overloads in z3++.h
• ee347735be8246d7150fa90b1e35cfc5f02bb835 remove junk
• eb8c63080a9f37e023fce58caf76e82e4497c406 Refactor and fix uninitialized variables and improve function consistency across multiple modules
• 499ed5d8445607c03c4bd11e5cba27a91dfec578 remove unneeded iterator functions
• 737c2208fad6c006a391897663adba71215f066f delete more default constructors
• 4b4a28239f9a06e9e10049f73f65e9859268b0a6 Add const qualifiers to comparison operators and update iterator equality checks in various classes
• a62fede64ba641cb6158f3bfdd22fd86f87d55f9 remove a few default constructors
• 22d9bfad358eefaa2f7aa490983463f6b0dd022f fix warning with iterators due to non-const comparator
• 11218154391d5137ab35a3281fb6283587c08ba0 Standardize C++20 flag across different platforms in build script
• 1e580a7f12cb1cbba6aed4d3484bae4988e06806 update to c++20, remove debug output
• 96c13757864c3fb5ec91e811fb4b4186fcd4ce91 #7391
• a9f8ec1bcb997ab7d386e67ff4825450b110728a updated handling of value initialization for bit-vectors
• ba5cec77045720d9cb81edbf102e473762762f37 additional rewrites for bv2int
• fa7fc8ef5ed98849f1a1408130f61a1b98bf58ca Refactor bv_rewriter functions using unified variable assignment and early break logic
• d66609ea14e8d329bb1ab730c93c98f3f67250be fix #7389
• 0c48a50d59f207e3f1dee38a02391fd21f038d5b Add support for initializing variable values in solver and optimize contexts in Z3
• 342dccdc0223b10f03369b037d529b396f70843b correctly process cancellation in gomory cuts
• b99c4a47a4097cc6a671808f1e8abafcfd54bd06 Add override specifiers to methods in set_initial_value_cmd class for clarity and consistency
• 8349ee006936f8088e2cbba66504bd2c8fc458a4 Add support for const array in all logics as per issue #7383
• 4896edfb042a44c05b57770d4f77298723071c28 Add tracking of values size in scoped_state push method in opt_context
• a3f35b6830fb9639a3e1d0dc23250e91973cb244 Add command to set initial value hints for solver in various components
• 1c163dbad2d2d9716a6a9eb7654a6a4387104ee3 remove output
• 0f896503a9ffe875936ec4f80094ea0e587e833a Add initial value setting API for solver and optimize contexts and update related function signatures
• 48712b4f60e090b3e95bb71063cbfe37c1c1d353 Add initial value setting for variables in Z3 API, solver, and optimize modules
• 0ba306e7b320901540162bfd7cf70c7b7399be17 y
• 99a9a4af03ed34fd4bd13b9881ca5910646d4c54 fix #7372
• 1ace3d0cf3f1a0f1c1c4a39a581674ebe7fa5306 fix #7372

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 4.next

• Planned features
  • sat.euf
    • a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. the current state is unstable. It lacks efficient ematching.
  • polysat
    • native word level bit-vector solving.
  • introduction of simple induction lemmas to handle a limited repertoire of induction proofs.

Version 4.13.2

• Performance regression fix. #7404

Version 4.13.1

• single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia.

• using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai.

  The projection is described in paper by Haokun Li and Bican Xia, Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection. The code ported from https://github.com/hybridSMT/hybridSMT.git

• Add API for providing hints for the solver/optimize contexts for which initial values to attempt to use for variables. The new API function are Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible. The SMTLIB front-end contains the new command (set-initial-value var value). For example, (declare-const x Int) (set-initial-value x 10) (push) (assert (> x 0)) (check-sat) (get-model) produces a model where x = 10. We use (push) to ensure that z3 doesn't run a specialized pre-processor that eliminates x, which renders the initialization without effect.

Version 4.13.0

• add ARM64 wheels for Python, thanks to Steven Moy, smoy

Version 4.12.6

• remove expensive rewrite that coalesces adjacent stores
• improved Java use of reference queues thanks to Thomas Haas #7131
• fixes to conditional import of python library thanks to Cal Jacobson #7116
• include universe for constants that get removed during pre-processing #7121
• code improvements, Bruce Mitchener #7119
• fix nested callback handling for user propagators
• include ARM64 binaries in distribution

... (truncated)

Commits

• 9a8ff74 update version number and release notes
• 11bb19d make default tactic cases lazy
• 40b0210 fixes to lazy tactic uses
• 01cf042 fix #7404, relates to #7400.
• d047b86 pypi publish
• f4452a0 pypi publish
• 3df7299 update signature of operator==
• 649c36a align nightly and release yamls
• 8d831a1 set to macos latest
• b39bcd6 remove ubuntu20
• 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 merge will merge this PR after your CI passes on it
• @dependabot squash and merge will squash and merge this PR after your CI passes on it
• @dependabot cancel merge will cancel a previously requested merge and block automerging
• @dependabot reopen will reopen this PR if it is closed
• @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
• @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)