Merge pull request ethereum#15537 from ethereum/cleanoutDynamicZ3Stuff

Remove remaining artifacts of dynamically loading Z3.

.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" -DUSE_Z3=OFF ..
+..\deps\cmake\bin\cmake -G "Visual Studio 16 2019" -DBoost_DIR="$boost_dir\" -DCMAKE_MSVC_RUNTIME_LIBRARY=MultiThreaded -DCMAKE_INSTALL_PREFIX="$PSScriptRoot\..\upload" ..
 if ( -not $? ) { throw "CMake configure failed." }
 msbuild solidity.sln /p:Configuration=Release /m:10 /v:minimal
 if ( -not $? ) { throw "Build failed." }

.circleci/config.yml

@@ -1049,7 +1049,7 @@ jobs:
     <<: *base_ubuntu2004_xlarge
     environment:
       <<: *base_ubuntu2004_xlarge_env
-      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -DUSE_Z3_DLOPEN=ON -DSOLC_STATIC_STDLIBS=ON
+      CMAKE_OPTIONS: -DCMAKE_BUILD_TYPE=Release -DSOLC_STATIC_STDLIBS=ON
     steps:
       - checkout
       - run_build
@@ -1110,8 +1110,6 @@ jobs:
     <<: *base_archlinux_large
     environment:
       <<: *base_archlinux_large_env
-      # This can be switched off if we run out of sync with Arch.
-      USE_Z3: ON
     steps:
       - run:
           name: Install build dependencies

cmake/EthCompilerSettings.cmake

@@ -260,9 +260,3 @@ if(COVERAGE)
 	endif()
 	add_compile_options(-g --coverage)
 endif()
-
-# SMT Solvers integration
-option(USE_Z3 "Allow compiling with Z3 SMT solver integration" ON)
-if(UNIX AND NOT APPLE)
-	option(USE_Z3_DLOPEN "Dynamically load the Z3 SMT solver instead of linking against it." OFF)
-endif()

cmake/FindZ3.cmake

@@ -1,51 +1,47 @@
-if (USE_Z3)
-    # Save and clear Z3_FIND_VERSION, since the
-    # Z3 config module cannot handle version requirements.
-    set(Z3_FIND_VERSION_ORIG ${Z3_FIND_VERSION})
-    set(Z3_FIND_VERSION)
-    # Try to find Z3 using its stock cmake files.
-    find_package(Z3 QUIET CONFIG)
-    # Restore Z3_FIND_VERSION for find_package_handle_standard_args.
-    set(Z3_FIND_VERSION ${Z3_FIND_VERSION_ORIG})
-    set(Z3_FIND_VERSION_ORIG)
+# Save and clear Z3_FIND_VERSION, since the
+# Z3 config module cannot handle version requirements.
+set(Z3_FIND_VERSION_ORIG ${Z3_FIND_VERSION})
+set(Z3_FIND_VERSION)
+# Try to find Z3 using its stock cmake files.
+find_package(Z3 QUIET CONFIG)
+# Restore Z3_FIND_VERSION for find_package_handle_standard_args.
+set(Z3_FIND_VERSION ${Z3_FIND_VERSION_ORIG})
+set(Z3_FIND_VERSION_ORIG)
 
-    include(FindPackageHandleStandardArgs)
+include(FindPackageHandleStandardArgs)
 
-    if (Z3_FOUND)
-        set(Z3_VERSION ${Z3_VERSION_STRING})
-        find_package_handle_standard_args(Z3 CONFIG_MODE)
-    else()
-        find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3)
-        find_library(Z3_LIBRARY NAMES z3)
-        find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin)
+if (Z3_FOUND)
+    set(Z3_VERSION ${Z3_VERSION_STRING})
+    find_package_handle_standard_args(Z3 CONFIG_MODE)
+else()
+    find_path(Z3_INCLUDE_DIR NAMES z3++.h PATH_SUFFIXES z3)
+    find_library(Z3_LIBRARY NAMES z3)
+    find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin)
 
-        if(Z3_INCLUDE_DIR AND Z3_LIBRARY)
-            if(Z3_EXECUTABLE)
-                execute_process (COMMAND ${Z3_EXECUTABLE} -version
-                    OUTPUT_VARIABLE libz3_version_str
-                    ERROR_QUIET
-                    OUTPUT_STRIP_TRAILING_WHITESPACE)
+    if(Z3_INCLUDE_DIR AND Z3_LIBRARY)
+        if(Z3_EXECUTABLE)
+            execute_process (COMMAND ${Z3_EXECUTABLE} -version
+                OUTPUT_VARIABLE libz3_version_str
+                ERROR_QUIET
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
 
-                string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1"
-                       Z3_VERSION_STRING "${libz3_version_str}")
-                unset(libz3_version_str)
-            else()
-                message(WARNING "Could not determine the version of z3, since the z3 executable was not found.")
-                set(Z3_VERSION_STRING "0.0.0")
-            endif()
+            string(REGEX REPLACE "^Z3 version ([0-9.]+).*" "\\1"
+                   Z3_VERSION_STRING "${libz3_version_str}")
+            unset(libz3_version_str)
+        else()
+            message(WARNING "Could not determine the version of z3, since the z3 executable was not found.")
+            set(Z3_VERSION_STRING "0.0.0")
         endif()
-        mark_as_advanced(Z3_VERSION_STRING z3_DIR)
+    endif()
+    mark_as_advanced(Z3_VERSION_STRING z3_DIR)
 
-        find_package_handle_standard_args(Z3
-            REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR
-            VERSION_VAR Z3_VERSION_STRING)
+    find_package_handle_standard_args(Z3
+        REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR
+        VERSION_VAR Z3_VERSION_STRING)
 
-        if (NOT TARGET z3::libz3)
-            add_library(z3::libz3 UNKNOWN IMPORTED)
-            set_property(TARGET z3::libz3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY})
-            set_property(TARGET z3::libz3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR})
-        endif()
+    if (NOT TARGET z3::libz3)
+        add_library(z3::libz3 UNKNOWN IMPORTED)
+        set_property(TARGET z3::libz3 PROPERTY IMPORTED_LOCATION ${Z3_LIBRARY})
+        set_property(TARGET z3::libz3 PROPERTY INTERFACE_INCLUDE_DIRECTORIES ${Z3_INCLUDE_DIR})
     endif()
-else()
-    set(Z3_FOUND FALSE)
 endif()

cmake/toolchains/libfuzzer.cmake

@@ -1,7 +1,5 @@
 # Inherit default options
 include("${CMAKE_CURRENT_LIST_DIR}/default.cmake")
-# Enable Z3
-set(USE_Z3 ON CACHE BOOL "Enable Z3" FORCE)
 # Build fuzzing binaries
 set(OSSFUZZ ON CACHE BOOL "Enable fuzzer build" FORCE)
 # Use libfuzzer as the fuzzing back-end

docs/installing-solidity.rst

@@ -527,23 +527,12 @@ If you are interested what CMake options are available run ``cmake .. -LH``.
 
 SMT Solvers
 -----------
-Solidity can be built against Z3 SMT solver and will do so by default if
-it is found in the system. Z3 can be disabled by a ``cmake`` option.
-
-*Note: In some cases, this can also be a potential workaround for build failures.*
-
-
-Inside the build folder you can disable Z3, since it is enabled by default:
-
-.. code-block:: bash
-
-    # disables Z3 SMT Solver.
-    cmake .. -DUSE_Z3=OFF
+Solidity can optionally use SMT solvers, namely ``z3``, ``cvc5`` and ``Eldarica``,
+but their presence is checked only at runtime, they are not needed for the build to succeed.
 
 .. note::
 
-    Solidity can optionally use other solvers, namely ``cvc5`` and ``Eldarica``,
-    but their presence is checked only at runtime, they are not needed for the build to succeed.
+    The emscripten builds require Z3 and will statically link against it instead.
 
 The Version String in Detail
 ============================