chore(deps): bump z3 to 4.13.0

[chenrui333]

• bump z3 to 4.13.0

• relates to solidity: use modern cmake syntax Homebrew/homebrew-core#183889

[github-actions]

Thank you for your contribution to the Solidity compiler! A team member will follow up shortly.

If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother.

If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix.

[cameel]

The procedure to update z3 is unfortunately a bit more complicated than this. It will require updating test expectations, and AFAIK Z3Prover/z3#7255 is still a blocker for this (@blishko is that still the case?).

It also cannot be easily done in an external PR, since we need the PR to trigger the base CI image rebuild via Github Actions. For this reason I'm going to close this. We still have #15198 open though, and we do intend to update when blockers are resolved.

[chenrui333]

@cameel got it, do you have any concerns that homebrew ship the binary built with z3 4.13.0 then? thanks!

[cameel]

Not really. The Z3 issue is about it hanging in some scenarios, but the output is still correct when you do get an answer. 4.12 might be a better choice if you hit those hanging cases but 4.13 has some improvements and bugfixes too so I can't even say that one is recommended over the other. Both versions are supported, we still support anything >= 4.8, it's just that 4.12 is still the one we run our tests against. The STRICT_Z3_VERSION option forces that specific version by default, but it can be disabled and is there mostly to guide people who don't have a strong preference to choose the one that can pass the test suite, which is unfortunately bound to a single version.