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 #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.