[llvm-bugs] [Bug 43464] New: Z3 prover not recognized when cmake configures LLVM 9 on Windows

via llvm-bugs llvm-bugs at lists.llvm.org
Thu Sep 26 06:26:13 PDT 2019


            Bug ID: 43464
           Summary: Z3 prover not recognized when cmake configures LLVM 9
                    on Windows
           Product: Build scripts
           Version: 9.0
          Hardware: PC
                OS: Windows NT
            Status: NEW
          Severity: enhancement
          Priority: P
         Component: cmake
          Assignee: unassignedbugs at nondot.org
          Reporter: man130117 at outlook.com
                CC: llvm-bugs at lists.llvm.org

Created attachment 22578
  --> https://bugs.llvm.org/attachment.cgi?id=22578&action=edit
New/modified FindZ3.cmake module

When cmake configures building LLVM 9, under Windows (10 Pro), with "x64 Native
Tools Command Prompt for VS 2019", it complains (among others) like this:

-- Could NOT find Z3: Found unsuitable version "0.0.0", but required is at
least "4.7.1" (found

and then Z3 is not used for building (though it is available as can be seen

I've found the reason of this in llvm/cmake/modules/FindZ3.cmake. Function 
"check_z3_version" in command "try_run" makes use of parameter: 

  "LINK_LIBRARIES -L${z3_lib_path} -lz3"

that finally creates a command line not understood by MSVC linker; the linker
fails to link and the function returns "0.0.0" as the Z3 version string.

I've changed the module a little (see attachment) to provide LINK_LIBRARIES in
a way suitable for MSVC, and now cmake finds Z3 correctly:

-- Found Z3: C:/Users/Marek/AppData/Local/Programs/z3-4.8.6-x64/bin/libz3.lib
(found suitable version "4.8.6", minimum required is "4.7.1")

Marek AnioĊ‚a

PS. Here is the diff between the original and the new module:

  2019-09-26 15:15:07.188000000 +0200
+++ C:\Users\Marek\Develop\llvm-project\llvm\cmake\modules\FindZ3.cmake
2019-09-26 15:15:08.110000000 +0200
@@ -13,16 +13,21 @@
           return 0;

-  # Get lib path
-  get_filename_component(z3_lib_path ${z3_lib} PATH)
+  if (MSVC)
+    set(z3_test_libs "${z3_lib}")
+  else()
+    # Get lib path
+    get_filename_component(z3_lib_path ${z3_lib} PATH)
+    set(z3_test_libs "-L${z3_lib_path} -lz3")
+  endif()
     COMPILE_DEFINITIONS -I"${z3_include}"
-    LINK_LIBRARIES -L${z3_lib_path} -lz3
+    LINK_LIBRARIES ${z3_test_libs}

You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20190926/d0e0129f/attachment.html>

More information about the llvm-bugs mailing list