[PATCH] D88198: Hints CMake where to find Z3 with LLVM_Z3_INSTALL_DIR.

Ella Ma via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Wed Sep 23 20:49:47 PDT 2020


OikawaKirie created this revision.
OikawaKirie added a reviewer: mikhail.ramalho.
OikawaKirie added a project: LLVM.
Herald added subscribers: llvm-commits, mgorny.
OikawaKirie requested review of this revision.

It seems that the variable LLVM_Z3_INSTALL_DIR was only used to print the error messages when Z3 is not found. In this patch, this variable is now actually used to hint CMake where to find `Z3Config.cake`.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D88198

Files:
  llvm/CMakeLists.txt


Index: llvm/CMakeLists.txt
===================================================================
--- llvm/CMakeLists.txt
+++ llvm/CMakeLists.txt
@@ -371,19 +371,20 @@
 )
 
 if (LLVM_ENABLE_Z3_SOLVER)
-  find_package(Z3 4.7.1)
-  
   if (LLVM_Z3_INSTALL_DIR)
+    find_package(Z3 4.7.1 HINTS ${LLVM_Z3_INSTALL_DIR})
     if (NOT Z3_FOUND)
       message(FATAL_ERROR "Z3 >= 4.7.1 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
     endif()
-  endif()
-  
-  if (NOT Z3_FOUND)
-    message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
+  else()
+    find_package(Z3 4.7.1)
+    if (NOT Z3_FOUND)
+      message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
+    endif()
   endif()
 
   set(LLVM_WITH_Z3 1)
+  message(STATUS "Found Z3 ${Z3_VERSION_STRING} in ${Z3_DIR}")
 endif()
 
 set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D88198.293932.patch
Type: text/x-patch
Size: 919 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200924/d14de5c1/attachment.bin>


More information about the llvm-commits mailing list