[PATCH] D54978: Move the SMT API to LLVM

Tue Feb 12 12:16:55 PST 2019

brzycki added a comment.

I think I found why others are struggling to recreate this issue. I did not have the package `z3/bionic` installed. This provides the `/usr/bin/z3` executable which `llvm/cmake/modules/FindZ3.cmake` relies upon to determine the correct `Z3_VERSION_STRING`.

If I perform the following on an unpatched checkout of sha b0a227049fda <https://reviews.llvm.org/rGb0a227049fda9d0d229ea801ae77bf1b812f7328> the build works :

  sudo apt install -y z3 libz3-4 libz3-dev
  mkdir build && cd build

Either of the following CMake commands build successfully:

  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm
  cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF ../llvm-project/llvm

And if I try `-D LLVM_ENABLE_Z3_SOLVER=ON` I receive a top-leve CMake error immediately:

  -- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so)
  CMake Error at CMakeLists.txt:406 (message):
    LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.

  -- Configuring incomplete, errors occurred!
  See also "/work/brzycki/build/CMakeFiles/CMakeOutput.log".
  ninja: error: loading 'build.ninja': No such file or directory

Unfortunately it's completely valid to install packages `libz3-4` and `libz3-dev` without pulling in `z3` on Ubuntu 18.04.  I've added this to my internal build notes.

I'm also looking to see if there's a way to better  handle this case inside the `find_package(Z3 ...)` subsystem of llvm.

Repository:
  rC Clang

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

https://reviews.llvm.org/D54978