Fixed Z3 version check crash

[Johanmyst]

The Z3 version check checks for an exact (string) match between the version number passed to --z3version X and the output of z3 --version (ignoring the Z3 version prefix and - 64 bit suffix ). This exact matching is too strict and incorrectly rejects some versions/builds of Z3 because they output additional information after the version number.

For example, the Z3 binary included by the Everest script outputs the following:

❯ z3 --version      
Z3 version 4.8.5 - 64 bit

However, the current Z3 binary on the Arch repositories outputs the following:

❯ z3-4.12.2 --version 
Z3 version 4.12.2 - 64 bit - build hashcode e417f7d78509b2d0c9ebc911fee7632e6ef546b6

The appended build hash code causes the version check in F* to fail. Changing the check from an exact match to a FStar.Compiler.Utils.starts_with check fixes this issue (perhaps a contains check would be better in case Z3 ever outputs anything before the version number, but I didn't think that was necessary).

[mtzguido]

Hi Johannes, thanks! I was surprised that the hash code is printed in the version with the get-info command, which is what F* checks, but it is:

# z3 -in
(get-info :version)
(:version "4.12.2 - build hashcode e417f7d78509b2d0c9ebc911fee7632e6ef546b6")

Just one thing, checking for the prefix will accept more versions than it should :) such as 4.12.11 if 4.12.1 is specified. Could we maybe instead split this string with " - " as a separator and grab the first component? I think BU.split should work for that. I could also do that if you prefer, just let me know.

[Johanmyst]

Hi Guido,

Ah, that's a good point. I've updated my fix to use BU.split instead (note that splitting by - requires also stripping the whitespace) and it seems to work properly in my tests.

Hope this help!

PS: The force-push is simply because I misconfigured my global git settings & "recommitted" instead of simply syncing.

[mtzguido]

Thanks! I was thinking using " - " as a separator to avoid the trim, but trimming is good in any case. No worries on the force push (it's better IMO). Merging.