brzycki added a comment.
In D54978#1392464 <https://reviews.llvm.org/D54978#1392464>, @Szelethus wrote:
> Shouldn't that be off by default?
The default for `LLVM_ENABLE_Z3_SOLVER` depends entirely on what CMake detects
from `find_package()`. Here is the relevant code in `llvm/CMakeLists.txt`:
find_package(Z3 4.7.1)
...
set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
option(LLVM_ENABLE_Z3_SOLVER
"Enable Support for the Z3 constraint solver in LLVM."
${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
)
If `find_package()` idenfiies a suitable `Z3_FOUND` the default is to enable
builds with the Z3 framework. In other words the entire Z3 feature is manual
opt-out and implicit opt-in when CMake thinks a suitable Z3 library is found.
In D54978#1393552 <https://reviews.llvm.org/D54978#1393552>, @ddcc wrote:
> The likely reason for this versioning problem is that the current versioning
> implementation in FindZ3.cmake is best-effort only.
Thank you @ddcc for this explanation. If that's the case I'd really prefer if
`LLVM_ENABLE_Z3_SOLVER` was explicit opt-in and defaulted to `OFF` regardless
of what `find_package` returned.
Repository:
rC Clang
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D54978/new/
https://reviews.llvm.org/D54978
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
