<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Hi,</div><div><br></div><div><div>Thank you for the discussion, I was finally able to reproduce the error.<br></div></div><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>Hello @ddcc.<br>I agree with your reasoning here and developed a patch based on this line of thought:<br>
<br>  diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake<br>  index 5c6d3f0b427..b213342df37 100644<br>  --- a/llvm/cmake/modules/FindZ3.cmake<br>  +++ b/llvm/cmake/modules/FindZ3.cmake<br>  @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)<br>       string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"<br>              Z3_VERSION_STRING "${libz3_version_str}")<br>       unset(libz3_version_str)<br>  +else()<br>  +    # The version could not be determined from running Z3_EXECUTABLE. Set the<br>  +    # version Z3 to the lowest possible value such that all checks for a<br>  +    # minimum version will fail.<br>  +    set(Z3_VERSION_STRING "0.0.0")<br>   endif()<br>
<br>   # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if<br>
<br>This works for everything I could throw at it. If you think it's reasonable I can open another ticket and have the code reviewed as a separate fix.<br>
<br></blockquote><div><br></div><div>This seems fine but I'm wondering if we can remove the binary requirement all together: is it possible to run a small program that would return EXIT_SUCCESS if the library is the correct version?</div><div><br></div><div>Something like:</div><div>```</div><div>#include <z3.h></div><div><br></div><div>int main()</div><div>{</div><div>  unsigned int major, minor, build, revision;</div><div>  Z3_get_version(&major, &minor, &build, &revision);</div><div>  </div><div><div>  if(major >= 4 && minor >= 7 && build >= 1)</div><div>    return EXIT_SUCCESS;</div></div><div><br></div><div>  return EXIT_FAILURE;</div><div>}</div><div>```</div><div><br></div><div>This would be part of FindZ3.cmake and would set Z3_FOUND.</div><div><br></div><div>Do you guys think it's possible? I'm almost certain it can be done with autotools, but I'm clueless when it comes to cmake.</div><div><br></div></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div></div></div></div></div>