[PATCH] D54978: Move the SMT API to LLVM

Fri Mar 15 13:55:22 PDT 2019

mikhail.ramalho added a comment.

Hi all,

Sorry for the massive delay, but I just updated the `FindZ3` script to retrieve the version from the lib. I changed it to use `try_run` instead of `try_compile` so we can get the version number.

I tried to use @brzycki code to get the version from the header, however, it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice `"Z3 4.8.3.0"` but in version 4.8.4 it's `"Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"` and cmake fails with the following message:

  -- Could NOT find Z3: Found unsuitable version "#define Z3_FULL_VERSION    "Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"", but required is at least "4.7.1" (found /home/mgadelha/z3/bin/libz3.so)

I believe we have a few options here:

1. Update the regex to handle the new format for `Z3_FULL_VERSION`.
2. Instead of parsing `Z3_FULL_VERSION`, we can parse `Z3_MAJOR_VERSION`, `Z3_MINOR_VERSION` and `Z3_BUILD_NUMBER` which are also available in the same header.

But, we'll still face the same problem of them changing the string format and breaking the scripts.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978