Z3 version check breaks if Z3 prints deprecation warnings

[Johanmyst]

Hi!

I'm posting this in reference to this slack channel discussion thread.

When building FStar (also through Opam), the version of Z3 is checked here. This check simply takes the output of z3 -version and if the output starts with the correct string, the check passes.

However, if Z3 prints anything else before the version number (such as deprecation warnings), this check fails. For example, when using the OpenMP library provided by LLVM version 15 (version 13 does not print this warning; I haven't checked version 14), this deprecation warning is printed: OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead. Because this warning is printed before Z3's normal output (even though it is correct), the version check fails and the build breaks.

Replacing the version check from BU.starts_with to BU.contains should likely fix this issue (defined in this module).

Kindly,

Johannes

[mtzguido]

Hi Johannes, thanks for the report!

The Z3 version check should really just raise a warning. Is the build breaking because of that, or during the Z3 test that F* does on startup?

If it's the latter, changing that line won't help, but maybe the solution is just to not put Z3's stderr into the same pipe as its stdout. (I imagine this warning goes to stderr... I'm building clang to check but maybe you can easily confirm too.)

[mtzguido]

Hi Johannes. This should now work, even with the warning, with the above PR merged. We are however working on upgrading a newer Z3 version (4.12), but that will take some time.