<html>
<head>
<base href="https://bugs.llvm.org/">
</head>
<body><table border="1" cellspacing="0" cellpadding="8">
<tr>
<th>Bug ID</th>
<td><a class="bz_bug_link
bz_status_NEW "
title="NEW - Z3 prover not recognized when cmake configures LLVM 9 on Windows"
href="https://bugs.llvm.org/show_bug.cgi?id=43464">43464</a>
</td>
</tr>
<tr>
<th>Summary</th>
<td>Z3 prover not recognized when cmake configures LLVM 9 on Windows
</td>
</tr>
<tr>
<th>Product</th>
<td>Build scripts
</td>
</tr>
<tr>
<th>Version</th>
<td>9.0
</td>
</tr>
<tr>
<th>Hardware</th>
<td>PC
</td>
</tr>
<tr>
<th>OS</th>
<td>Windows NT
</td>
</tr>
<tr>
<th>Status</th>
<td>NEW
</td>
</tr>
<tr>
<th>Severity</th>
<td>enhancement
</td>
</tr>
<tr>
<th>Priority</th>
<td>P
</td>
</tr>
<tr>
<th>Component</th>
<td>cmake
</td>
</tr>
<tr>
<th>Assignee</th>
<td>unassignedbugs@nondot.org
</td>
</tr>
<tr>
<th>Reporter</th>
<td>man130117@outlook.com
</td>
</tr>
<tr>
<th>CC</th>
<td>llvm-bugs@lists.llvm.org
</td>
</tr></table>
<p>
<div>
<pre>Created <span class=""><a href="attachment.cgi?id=22578" name="attach_22578" title="New/modified FindZ3.cmake module">attachment 22578</a> <a href="attachment.cgi?id=22578&action=edit" title="New/modified FindZ3.cmake module">[details]</a></span>
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
C:/Users/Marek/AppData/Local/Programs/z3-4.8.6-x64/bin/libz3.lib)
and then Z3 is not used for building (though it is available as can be seen
above).
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:
---
C:\Users\Marek\AppData\Local\Temp\smartgit-2473644940642043647tmp\compare\FindZ3-index--6400871964085648525.cmake
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()
+
try_run(
Z3_RETURNCODE
Z3_COMPILED
${CMAKE_BINARY_DIR}
${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
COMPILE_DEFINITIONS -I"${z3_include}"
- LINK_LIBRARIES -L${z3_lib_path} -lz3
+ LINK_LIBRARIES ${z3_test_libs}
RUN_OUTPUT_VARIABLE SRC_OUTPUT
)</pre>
</div>
</p>
<hr>
<span>You are receiving this mail because:</span>
<ul>
<li>You are on the CC list for the bug.</li>
</ul>
</body>
</html>