[PATCH] D54978: Move the SMT API to LLVM
Brian Rzycki via Phabricator via llvm-commits
llvm-commits at lists.llvm.org
Mon Feb 11 13:11:27 PST 2019
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`:
"Enable Support for the Z3 constraint solver in LLVM."
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.
CHANGES SINCE LAST ACTION
More information about the llvm-commits