Support Z3, version 4.8.11

[xgqt]

Based on my tests and conversation from https://github.com/FStarLang/FStar/issues/2344 F* does not yet support Z3 4.8.11.

Are there any plans as of now to port to newer versions?

[kant2002]

What's the plan to update to latest z3? Does it needs to be in one go, or we can gradually bump versions until we reach latest one?

[aseemr]

We are looking at upgrading to the latest 4.8.15 release. It is a bit involved because it requires accommodating other projects that are part of our CI. Will keep posting updates as we make progress!

[shonfeder]

Hi! I thought it might be worth noting that the dependency on z3 4.8.5 prevents using fstar with OCaml 5.

To update the state of Z3 on opam now: the latest z3 available on opam is 4.12.2-1, but assuming there is need to stay on 4.8, the latest would now be 4.8.17.

(I'd be happy to lend a hand on the effort to update here, if that could be useful.)

[mtzguido]

Hi, we are actually making progress here and have most of the infrastructure set up to use a new Z3. Here's some more detail: https://github.com/FStarLang/FStar/discussions/2974 and https://github.com/FStarLang/FStar/pull/2995.

The current status is that you can use --z3version 4.12.3 to make F* try to find z3-4.12.3in the PATH and use it (if it exists, or default to z3 as usual). F* also passes some new needed config flags to Z3 to not regress in many proofs. So, if you install a new version and pass this flag everywhere (or even modify the default in FStar.Options.fst) you should be able to use a new Z3 from their master branch. Though I think 4.12.2 does not include the extra config flags... so YMMV. It's probably easier to install 4.12.3.

We have not switched the default version to the latest one as there's still one regression for which we haven't identified the cause, it's probably a Z3 regression. I'll try to do that soon and make a PR for upgrading the default.

[shonfeder]

Oh that’s awesome! Thanks for the info and congrats and on nearing the end of the update :)