update Z3 to version 3.12.1

The pre-compiled Linux version of Z3 3.12.1 requires glibc in version 2.35,
which is not available on older systems like Ubuntu 18.04, Ubuntu 20.04, Debian 10, or Debian 11.

As a solution, we provide a self-compiled Linux version depending on the older GLIBC 2.27.
This allows JavaSMT with Z3 to be executed on some more systems.

With the self-compiled library we can simplify the loading condition for Z3 in our JUnit tests.

doc/Developers-How-to-Release-into-Ivy.md

@@ -59,7 +59,25 @@ ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION
 ```
 Finally follow the instructions shown in the message at the end.
 
-#### Optional
+#### Optional (from source for Linux target with older GLIBC)
+This step is for the following use case:
+Newer releases of Z3 depend on newer versions of GLIBC (>=v2.35),
+so we want to compile the Linux release on our own and then combine it with the provided libraries for Windows and MacOS.
+We follow the steps from above, download and unpack the given zip archives for all platforms, except the Linux release (where the GLIBC is too new).
+For simple usage, we provide a Docker definition/environment under `/docker` (based on Ubuntu 18.04 with GLIBC 2.27),
+in which the following build command can be run in the unpacked source directory:
+```
+python3 scripts/mk_make.py --java && cd build && make -j 2
+```
+Afterwards copy the native libraries for Linux (`libz3.so` and `libz3java.so`) from the directory `./build` into `./bin`.
+Then perform as written above with adding the additional pre-compiled binaries for other operating systems,
+and publish the directory `./bin` with an ant command like the one from above:
+```
+ant publish-z3 -Dz3.path=$Z3_DIR/bin -Dz3.version=$Z3_VERSION-glibc_2.27
+```
+
+
+#### Optional (outdated: from source for Linux target)
 To publish Z3 from source, [download it](https://github.com/Z3Prover/z3) and build
 it with the following command in its directory on a 64bit Ubuntu 16.04 system:
 ```

lib/ivy.xml

@@ -158,7 +158,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.8" conf="runtime-mathsat->solver-mathsat" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.11.2" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.12.1-glibc_2.27" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.2-g40f1137e5" conf="runtime-cvc5->solver-cvc5" />

src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java

@@ -19,7 +19,6 @@
 import org.junit.runners.Parameterized;
 import org.junit.runners.Parameterized.Parameter;
 import org.junit.runners.Parameterized.Parameters;
-import org.sosy_lab.common.NativeLibraries;
 import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
@@ -99,30 +98,12 @@ private void requireSupportedOperatingSystem() {
         return;
       case Z3:
         assume.that(IS_LINUX || IS_WINDOWS || IS_MAC).isTrue();
-        if (IS_LINUX) {
-          assume.that(isSufficientVersionOfLibcxx()).isTrue();
-        }
         return;
       default:
         throw new AssertionError("unexpected solver: " + solverToUse());
     }
   }
 
-  /**
-   * The official Z3 release does only run with GLIBCXX in version 3.4.26 or newer. This excludes
-   * Ubuntu 18.04.
-   */
-  private boolean isSufficientVersionOfLibcxx() {
-    try {
-      NativeLibraries.loadLibrary("z3");
-    } catch (UnsatisfiedLinkError e) {
-      if (e.getMessage().contains("version `GLIBCXX_3.4.26' not found")) {
-        return false;
-      }
-    }
-    return true;
-  }
-
   @Before
   public final void initSolver() throws InvalidConfigurationException {
     config = Configuration.builder().setOption("solver.solver", solverToUse().toString()).build();