Merge pull request #11873 from soroosh-sdi/cmake-check-z3-latest

Require latest Z3 by default and allow relaxing the requirement with `STRICT_Z3_VERSION=OFF`

.circleci/build_win.ps1

@@ -18,7 +18,7 @@ else {
 mkdir build
 cd build
 $boost_dir=(Resolve-Path $PSScriptRoot\..\deps\boost\lib\cmake\Boost-*)
-..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" ..
+..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" -DUSE_Z3=OFF ..
 if ( -not $? ) { throw "CMake configure failed." }
 msbuild solidity.sln /p:Configuration=Release /m:5 /v:minimal
 if ( -not $? ) { throw "Build failed." }

CMakeLists.txt

@@ -34,6 +34,7 @@ endif()
 
 option(SOLC_LINK_STATIC "Link solc executable statically on supported platforms" OFF)
 option(SOLC_STATIC_STDLIBS "Link solc against static versions of libgcc and libstdc++ on supported platforms" OFF)
+option(STRICT_Z3_VERSION "Use the latest version of Z3" ON)
 
 # Setup cccache.
 include(EthCcache)
@@ -63,8 +64,29 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
 
 include(EthOptions)
 configure_project(TESTS)
+set(LATEST_Z3_VERSION "4.8.12")
+set(MINIMUM_Z3_VERSION "4.8.0")
+find_package(Z3)
+if (${Z3_FOUND})
+  if (${STRICT_Z3_VERSION})
+    if (NOT ("${Z3_VERSION_STRING}" VERSION_EQUAL ${LATEST_Z3_VERSION}))
+      message(
+        FATAL_ERROR
+        "SMTChecker tests require Z3 ${LATEST_Z3_VERSION} for all tests to pass.\n\
+Build with -DSTRICT_Z3_VERSION=OFF if you want to use a different version. \
+You can also use -DUSE_Z3=OFF to build without Z3. In both cases use --no-smt when running tests."
+      )
+    endif()
+  else()
+    if ("${Z3_VERSION_STRING}" VERSION_LESS ${MINIMUM_Z3_VERSION})
+      message(
+        FATAL_ERROR
+        "Solidity requires Z3 ${MINIMUM_Z3_VERSION} or newer. You can also use -DUSE_Z3=OFF to build without Z3."
+      )
+    endif()
+  endif()
+endif()
 
-find_package(Z3 4.8.0)
 if(${USE_Z3_DLOPEN})
   add_definitions(-DHAVE_Z3)
   add_definitions(-DHAVE_Z3_DLOPEN)

docs/installing-solidity.rst

@@ -336,6 +336,16 @@ The following are dependencies for all builds of Solidity:
 
     Starting from 0.5.10 linking against Boost 1.70+ should work without manual intervention.
 
+.. note::
+    The default build configuration requires a specific Z3 version (the latest one at the time the
+    code was last updated). Changes introduced between Z3 releases often result in slightly different
+    (but still valid) results being returned. Our SMT tests do not account for these differences and
+    will likely fail with a different version than the one they were written for. This does not mean
+    that a build using a different version is faulty. If you pass ``-DSTRICT_Z3_VERSION=OFF`` option
+    to CMake, you can build with any version that satisfies the requirement given in the table above.
+    If you do this, however, please remember to pass the ``--no-smt`` option to ``scripts/tests.sh``
+    to skip the SMT tests.
+
 Minimum Compiler Versions
 ^^^^^^^^^^^^^^^^^^^^^^^^^