[PATCH] D54978: Move the SMT API to LLVM
Brian Rzycki via Phabricator via llvm-commits
llvm-commits at lists.llvm.org
Tue Feb 12 12:16:54 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.
CHANGES SINCE LAST ACTION
More information about the llvm-commits