Fixed Z3 version check again

[Johanmyst]

A recent commit (#d6991a4) reverted a previous change to the Z3 version checking, which causes some Z3 builds to fail the check even though the version is correct.

The change in #d6991a4 removed splitting the output of z3-<version> --version on the - character. With the Z3 binaries pulled by the Everest build system, this isn't a problem because they simply output the version number. However, if you build Z3 manually, the --version command often outputs additional information, like the build hash (e.g. Z3 version 4.13.3 - 64 bit - build hashcode 4d30f26f72ce62f5dcb5a5258f632f84858714f).

This commit reverts this change and re-inserts the string-splitting such that custom Z3 builds (of the correct version) are supported again.

[mtzguido]

Hi Johan, sorry for the breakage. I'm confused though, we're using the directive (get-info :version) (instead of using --version) and in a local build it outputs a plain version number:

$ echo '(get-info :version)' | /home/guido/src/z3/build/z3 -in
(:version "4.13.4")

(on z3 commit 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571, which is not a tag). Can you say more on how you built z3 for this to fail, and what exactly you get? Not against the patch at all, just want to add a proper comment so we don't break it again.

Thanks!

[Johanmyst]

Hi Guido,

Sorry for the force-push; I tried updating with the upstream commits but forgot to rebase so unintentionally created a merge commit. I've rebased now so merging this pull request should be easier. Let me know if you'd like me to make any other changes/documentation additions for this pull request!

I'm confused though, we're using the directive (get-info :version) (instead of using --version)

True, but the output of this is the same as calling /path/to/z3-bin --version. As such, if that binary outputs more than purely the expected version string, the check on line 181 fails.

and in a local build it outputs a plain version number:

$ echo '(get-info :version)' | /home/guido/src/z3/build/z3 -in
(:version "4.13.4")

(on z3 commit 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571, which is not a tag).

I checked out and built the version of this exact commit:

$ git clone https://github.com/Z3Prover/z3.git ./z3
$ git checkout 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571
$ cmake -G "Ninja" -S ./ -B build -DCMAKE_INSTALL_PREFIX=./install -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++
$ cmake --build build
$ cmake --install build

If I then run the binary itself with ./install/bin/z3 --version, the output is: Z3 version 4.13.4 - 64 bit - build hashcode 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571. Similarly, if I run echo '(get-info :version)' | ./install/bin/z3 -in, the output is: (:version "4.13.4 - build hashcode 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571"). If I do the same with the z3 binaries included/pulled by the Everest scripts, the build hashcode ... part isn't shown.

I figured out that this is — at least partly — because the build system I used was cmake and/or clang/clang++. While z3 recommends using the CMake build system for most tasks (Z3 has a build system using CMake. Read the [README-CMake.md](https://github.com/Z3Prover/z3/blob/master/README-CMake.md) file for details. It is recommended for most build tasks, except for building OCaml bindings.), I can also build z3 like this:

$ git clone https://github.com/Z3Prover/z3.git ./z3
$ git checkout 6d3cfb63daa9afdd7d6d6b4d2f2fb84bd7324571
$ python3 ./scripts/mk_make.py
$ cd build
$ make -j$(nproc)

In this case, the output of ./build/z3 --version is Z3 version 4.13.4 - 64 bit and the output of echo '(get-info :version)' | ./build/z3 -in is (:version "4.13.4").

My fix simply splits the string on the first - character and only compares the string prior to that. Of course, should z3 change the format of the output, this will again break. Perhaps checking if the expected version string is a substring of the version check output, or whether the output starts with "Z3 version ...", would be better, but I doubt it makes a huge difference in practice.

Anyway, please let me know if there's anything you'd like me to change about my pull request!

Kindly,

Johannes

[mtzguido]

Thanks Johan! Just added a comment to this PR, will merge.