Why3 does not accept unknown versions of Z3
In the past, Why3 was accepting versions of provers that were not already known, with a message "use at your own risks" or something like that (maybe something less scary).
In version 1.4.0, it seems to continue to accept say Alt-Ergo 2.4.1, whereas Z3 versions higher than 4.8.10 are silently ignored.
An investigation by doing why3 config show
seems to indicate that the counterexample
alternative of Z3 is recognized, but not the others (i.e. the default one and the noBV
one). That may explain the difference with Alt-Ergo, because the latter has no counterexample
alternative.