Bump z3-solver from 4.13.2.0 to 4.13.3.0

[dependabot]

Bumps z3-solver from 4.13.2.0 to 4.13.3.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

• 3a8195b9c3875cbce4fe6a89c6874923d34479a9 #7419
• 7a0b58bcd5e28ce819a58832b8a2a61e6ad26595 increment minor version number
• efde65603622ae54ef82050b0ade3f3218b2d54b fix recursive self call for slice_solver check-sat-cc method

This list of changes was auto generated.

z3-4.13.3

4.13.3 release

Changes:

• 54d30f26f72ce62f5dcb5a5258f632f84858714f add _0 to platform tag for pypi
• 6e3b99fb9ee02cbc37c6fb3ba289a5fd0fb59134 downgrade to macos13 in builds until fully supported by pypi
• b268b56519f09828cc3b41d989b89377fae178cc update release notes
• 00f1f1b83da7c583d0290280b1b3bbb6097a6be8 fix typo in setup.py
• fe71b75ffdaaa775b8ff931b3d411aee7dcc13ff remove : from setup.py
• 5dc1b1acd4dfb0b6db110251883853f4b1274b14 remove hard-wired osx=11.0
• 48aa2f6988f62466ecfed284587357d4ca0722f2 setup python dist to remove internal build suffix for macos
• da614c65e58b8e97d6d0c7aaf3a1294bac8e6097 remove m_level attribute, use s->get_scope_level directly
• 6bd46b0922a0c02dbf142c4ac3dd7b9cca6d0b4c fix #7363. Replay relevancy on unit literals that are re-asserted during backtracking.
• cfd00ad672dbe1334976c35867001e3f96f63692 add slice solver option to command context

• 8a95dd4d65d0a4d9eaf760ebcd5ddf5456a17780 A slice solver option for interactive use case
• 0fec7efc7ba75de1292b78fe334a87a884a2187f micro-tuning
• c6cd25c822a552d0caf813d33b89e086d05750d9 mico-tuning
• 24d7b05c0d4e1eb07b2c6b11dd19c0aba4f9a603 refactor and optimize git operations for commit messages and failure analysis (#7412)
• 2ae4ac8d0a24b6542306737501bcc2679e34fcd2 fix build
• b60e1a2ed22111fefa328cfcbdc3fa1cdd2b1555 fixup variables
• 969511ac00830a97f49be9d9585540f33b8aaa7e fixup std-order / inv-order
• 66bb3109662ff2ff1c25de128b5e3ebc270334eb reset before manager is deallocated
• a98c9250690f82a67e27b5d8ae84d61550ffdfd7 optimize var_subst
• f5db6bf92b88a9648ae73de38d7a9989233a0922 install Julia for macos build
• e58eb9f3029a7055b9070a235aced7241d4ee5c3 fix indentation for mbp
• 3586b613f7e0cdd404d9c44e51d27d01be08019e remove default destructors
• b170f101481c51e4d753212b484bc5a48191f6ed reorder template definition
• 6dec943b297f455b178b2f0369544e99b0d79779 Bump docker/build-push-action from 6.7.0 to 6.9.0 (#7408)
• d686e92bfa48eac2c980b103a7c121387e83d851 disambiguate
• 93ff89bf9807ca305b49faae77f379f0bfab36ac add == for const_ref and ref to disambiguate equality.
• c7af97364a55394396b69feb04c449aa3fe60f1f fixes for #7402
• 328616b8b28feddca2fdb55b2865ca525d584e91 fix build warnings
• 8c39863019f32c12ae11869a38598849c2c2b404 fix typo in arch for setup.py
• 4cefc513eb24e6077ec77d6282a5cbfd212c886d add sequoia to os versions #7407
• 19f63cd6e336e5795c3a65fd0af1254e78a3ded2 add sequoia to os versions #7407
• 86b97186b0a4b3a8f8a041f2443b540952a5c530 fix build warnings

... (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.3

• Fixes, including #7363
• Fix paths to Java binaries in release
• Remove internal build names from pypi wheels

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

... (truncated)

Commits

• 54d30f2 add _0 to platform tag for pypi
• 6e3b99f downgrade to macos13 in builds until fully supported by pypi
• b268b56 update release notes
• 00f1f1b fix typo in setup.py
• fe71b75 remove : from setup.py
• 5dc1b1a remove hard-wired osx=11.0
• 48aa2f6 setup python dist to remove internal build suffix for macos
• da614c6 remove m_level attribute, use s->get_scope_level directly
• 6bd46b0 fix #7363. Replay relevancy on unit literals that are re-asserted during back...
• cfd00ad add slice solver option to command context
• 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)