Old Z3 is not supported (should enforce in CMake)

[axic]

I have z3 4.8.13 installed.

CMake properly warns (I think for the reason that different versions may produce different outputs for the tests):

  CMake Error at CMakeLists.txt:74 (message):
    SMTChecker tests require Z3 4.8.17 for all tests to pass.

    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.

However disabling it (using -DSTRICT_Z3_VERSION=OFF) shows that 4.8.13 is not a supported version anymore:

  /Projects/solidity/libsmtutil/Z3Interface.cpp:381:11: error: use of undeclared identifier 'Z3_OP_RECURSIVE'
                  kind == Z3_OP_RECURSIVE
                          ^

Should add another version check for "not older than".

[ekpyron]

Actually, in this particular case, we could even consider using a preprocessor check to still support compiling against older versions of the 4.8 series. IIRC (pinging @leonardoalt) it was mainly a matter of this exact enum part to be introduced - but things should reasonably work for older versions by just conditionally not checking for that enum value, right?

However, attempting to compile against any version <4.8.0, i.e. against a mismatching minor version, should be an error, we should also verify that that's the case.

[ekpyron]

For reference: basically the change in https://github.com/ethereum/solidity/pull/13009 could be put inside a preprocessor check for the appropriate Z3 version.

[leonardoalt]

Actually, in this particular case, we could even consider using a preprocessor check to still support compiling against older versions of the 4.8 series. IIRC (pinging @leonardoalt) it was mainly a matter of this exact enum part to be introduced - but things should reasonably work for older versions by just conditionally not checking for that enum value, right?

However, attempting to compile against any version <4.8.0, i.e. against a mismatching minor version, should be an error, we should also verify that that's the case.

Yea agree with that.

[Andy53]

This is currently in CMakeLists:

set(LATEST_Z3_VERSION "4.11.0")
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()

I think this covers this issue however if that is not the case can someone please elaborate on where this is lacking? I have been able to build solidity using version 4.11.0 and 4.9.1. Both built however the only issue I ran into is that when building Z3 from source or using the latest release they cause an error since they are newer than 4.11.0 (4.11.3/4.11.2).

Is it worth us just updating LATEST_Z3_VERSION to 4.11.3?

[blishko]

After #15252, I think we can close this issue?