build: package Z3 solver native libraries

27 files changed, 738 insertions, 1 deletions

diff --git a/buildSrc/src/main/kotlin/tools/refinery/gradle/internal/java-conventions.gradle.kts b/buildSrc/src/main/kotlin/tools/refinery/gradle/internal/java-conventions.gradle.kts
index 3df17d67..b149a483 100644
--- a/buildSrc/src/main/kotlin/tools/refinery/gradle/internal/java-conventions.gradle.kts
+++ b/buildSrc/src/main/kotlin/tools/refinery/gradle/internal/java-conventions.gradle.kts
@@ -101,6 +101,14 @@ tasks {
 publishing.publications {
         create<MavenPublication>("mavenJava") {
                 from(components["java"])
+                pom {
+                        licenses {
+                                license {
+                                        name = "Eclipse Public License - v 2.0"
+                                        url = "https://www.eclipse.org/legal/epl-2.0/"
+                                }
+                        }
+                }
         }
 }
 
diff --git a/buildSrc/src/main/kotlin/tools/refinery/gradle/interpreter-library.gradle.kts b/buildSrc/src/main/kotlin/tools/refinery/gradle/interpreter-library.gradle.kts
index ae30ff1b..8bafa1a5 100644
--- a/buildSrc/src/main/kotlin/tools/refinery/gradle/interpreter-library.gradle.kts
+++ b/buildSrc/src/main/kotlin/tools/refinery/gradle/interpreter-library.gradle.kts
@@ -8,7 +8,6 @@ package tools.refinery.gradle
 import tools.refinery.gradle.utils.SonarPropertiesUtils
 
 plugins {
-        id("maven-publish")
         id("tools.refinery.gradle.java-library")
         id("tools.refinery.gradle.sonarqube")
 }
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 6e5a72e9..11b188ea 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -33,3 +33,5 @@ for (project in rootProject.children) {
         project.name = "${rootProject.name}-$projectName"
         project.projectDir = file("subprojects/$projectName")
 }
+
+includeBuild("z3")
diff --git a/z3/build.gradle.kts b/z3/build.gradle.kts
new file mode 100644
index 00000000..74ee6bc8
--- /dev/null
+++ b/z3/build.gradle.kts
@@ -0,0 +1,9 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        alias(libs.plugins.versions)
+}
diff --git a/z3/buildSrc/build.gradle.kts b/z3/buildSrc/build.gradle.kts
new file mode 100644
index 00000000..adc19562
--- /dev/null
+++ b/z3/buildSrc/build.gradle.kts
@@ -0,0 +1,18 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        `kotlin-dsl`
+        alias(libs.plugins.versions)
+}
+
+repositories {
+        mavenCentral()
+}
+
+dependencies {
+        implementation(libs.asm)
+}
diff --git a/z3/buildSrc/settings.gradle.kts b/z3/buildSrc/settings.gradle.kts
new file mode 100644
index 00000000..095ab24c
--- /dev/null
+++ b/z3/buildSrc/settings.gradle.kts
@@ -0,0 +1,13 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+dependencyResolutionManagement {
+        versionCatalogs {
+                create("libs") {
+                        from(files("../gradle/libs.versions.toml"))
+                }
+        }
+}
diff --git a/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java b/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java
new file mode 100644
index 00000000..5ac56005
--- /dev/null
+++ b/z3/buildSrc/src/main/java/tools/refinery/z3/gradle/ClassFilePatcher.java
@@ -0,0 +1,48 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+package tools.refinery.z3.gradle;
+
+import org.objectweb.asm.*;
+
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.FileOutputStream;
+import java.io.IOException;
+
+public final class ClassFilePatcher {
+        private ClassFilePatcher() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static void removeClassInitializer(File classFile) throws IOException {
+                byte[] resultBytes;
+                try (var fileReader = new FileInputStream(classFile)) {
+                        var classReader = new ClassReader(fileReader);
+                        var classWriter = new ClassWriter(classReader, 0);
+                        var classVisitor = new Visitor(classWriter);
+                        classReader.accept(classVisitor, 0);
+                        resultBytes = classWriter.toByteArray();
+                }
+                try (var fileWriter = new FileOutputStream(classFile)) {
+                        fileWriter.write(resultBytes);
+                }
+        }
+
+        private static class Visitor extends ClassVisitor {
+                protected Visitor(ClassVisitor classVisitor) {
+                        super(Opcodes.ASM9, classVisitor);
+                }
+
+                @Override
+                public MethodVisitor visitMethod(int access, String name, String descriptor, String signature,
+                                                                                 String[] exceptions) {
+                        if (name.equals("<clinit>")) {
+                                return null;
+                        }
+                        return super.visitMethod(access, name, descriptor, signature, exceptions);
+                }
+        }
+}
diff --git a/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts b/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts
new file mode 100644
index 00000000..75d64a6f
--- /dev/null
+++ b/z3/buildSrc/src/main/kotlin/tools/refinery/z3/gradle/java-library.gradle.kts
@@ -0,0 +1,75 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+package tools.refinery.z3.gradle
+
+plugins {
+        `java-library`
+        `maven-publish`
+}
+
+java {
+        toolchain {
+                languageVersion.set(JavaLanguageVersion.of(21))
+        }
+}
+
+repositories {
+        mavenCentral()
+
+        // Configuration based on https://stackoverflow.com/a/34327202 to pretend that GitHub is an Ivy repository
+        // in order to take advantage of Gradle dependency caching.
+        val github = ivy {
+                setUrl("https://github.com")
+                patternLayout {
+                        artifact("/[organisation]/[module]/releases/download/[module]-[revision]/[classifier].[ext]")
+                        artifact("/[organisation]/[module]/archive/refs/tags/[module]-[revision].[ext]")
+                }
+                metadataSources {
+                        artifact()
+                }
+        }
+
+        exclusiveContent {
+                forRepositories(github)
+                filter {
+                        includeGroup("Z3Prover")
+                }
+        }
+}
+
+val z3: Provider<Configuration> by configurations.registering {
+        isCanBeConsumed = false
+        isCanBeResolved = true
+}
+
+tasks {
+        jar {
+                manifest {
+                        attributes(
+                                        "Bundle-SymbolicName" to "${project.group}.${project.name}",
+                                        "Bundle-Version" to project.version
+                        )
+                }
+        }
+}
+
+publishing.publications {
+        register<MavenPublication>("mavenJava") {
+                from(components["java"])
+                pom {
+                        licenses {
+                                license {
+                                        name = "MIT License"
+                                        url = "https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt"
+                                }
+                                license {
+                                        name = "The Apache License, Version 2.0"
+                                        url = "http://www.apache.org/licenses/LICENSE-2.0.txt"
+                                }
+                        }
+                }
+        }
+}
diff --git a/z3/docker/.gitignore b/z3/docker/.gitignore
new file mode 100644
index 00000000..d5b53f81
--- /dev/null
+++ b/z3/docker/.gitignore
@@ -0,0 +1,5 @@
+# SPDX-FileCopyrightText: 2023 The Refinery Authors
+#
+# SPDX-License-Identifier: CC0-1.0
+
+out/
diff --git a/z3/docker/README.md b/z3/docker/README.md
new file mode 100644
index 00000000..d979fd5e
--- /dev/null
+++ b/z3/docker/README.md
@@ -0,0 +1,14 @@
+<!--
+  SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+
+  SPDX-License-Identifier: Apache-2.0
+-->
+
+# Scripts for cross-building Z3 for linux-aarch64
+
+We intentionally build in Ubuntu Focal to avoid a dependency on glibc 2.35.
+See https://github.com/Z3Prover/z3/issues/6572 for details.
+
+This should not be necessary once Z3 4.12.3 is released, as now Z3 nighly
+includes linux-aarch64 builds.
+See https://github.com/Z3Prover/z3/issues/6835 for details.
diff --git a/z3/docker/build_in_docker.sh b/z3/docker/build_in_docker.sh
new file mode 100755
index 00000000..cd28bd32
--- /dev/null
+++ b/z3/docker/build_in_docker.sh
@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+# SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+set -euo pipefail
+
+z3_version="$1"
+target_uid="$2"
+target_gid="$3"
+
+apt-get update
+apt-get install -y python3 make gcc-aarch64-linux-gnu g++-aarch64-linux-gnu unzip
+wget "https://github.com/Z3Prover/z3/archive/refs/tags/z3-${z3_version}.zip"
+unzip "z3-${z3_version}.zip"
+cd "z3-z3-${z3_version}"
+CXX=aarch64-linux-gnu-g++ CC=aarch64-linux-gnu-gcc python3 scripts/mk_unix_dist.py -f --nodotnet --arch=arm64
+cp --preserve=all "./dist/z3-${z3_version}-arm64-glibc-2.31/bin"/*.so /data/out/
+chown "${target_uid}:${target_gid}" /data/out/*
+
diff --git a/z3/docker/cross_build.sh b/z3/docker/cross_build.sh
new file mode 100755
index 00000000..fe5edd2f
--- /dev/null
+++ b/z3/docker/cross_build.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+# SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+set -euo pipefail
+
+z3_version="$(grep '^version=' ../gradle.properties | cut -d'=' -f2)"
+
+rm -rf out
+mkdir out
+docker run --platform linux/amd64 --rm -it -v "${PWD}:/data" --entrypoint /bin/bash docker.io/eclipse-temurin:17-jdk-focal /data/build_in_docker.sh "${z3_version}" "$(id -u)" "$(id -g)"
+rm -rf ../subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/*
+cp ./out/* ../subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/
+
diff --git a/z3/gradle.properties b/z3/gradle.properties
new file mode 100644
index 00000000..3ef49dc6
--- /dev/null
+++ b/z3/gradle.properties
@@ -0,0 +1,9 @@
+# SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+file.encoding=UTF-8
+group=tools.refinery.z3
+org.gradle.configuration-cache=false
+org.gradle.parallel=true
+version=4.12.2
diff --git a/z3/gradle/libs.versions.toml b/z3/gradle/libs.versions.toml
new file mode 100644
index 00000000..88cf8083
--- /dev/null
+++ b/z3/gradle/libs.versions.toml
@@ -0,0 +1,15 @@
+# SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+[versions]
+junit = "5.10.1"
+
+[libraries]
+asm = { group = "org.ow2.asm", name = "asm", version = "9.6" }
+jna = { group = "net.java.dev.jna", name = "jna", version = "5.13.0" }
+junit-api = { group = "org.junit.jupiter", name = "junit-jupiter-api", version.ref = "junit" }
+junit-engine = { group = "org.junit.jupiter", name = "junit-jupiter-engine", version.ref = "junit" }
+
+[plugins]
+versions = { id = "com.github.ben-manes.versions", version = "0.50.0" }
diff --git a/z3/settings.gradle.kts b/z3/settings.gradle.kts
new file mode 100644
index 00000000..a857f5ce
--- /dev/null
+++ b/z3/settings.gradle.kts
@@ -0,0 +1,22 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+rootProject.name = "refinery-z3"
+
+include(
+                "solver",
+                "solver-darwin-aarch64",
+                "solver-darwin-x86-64",
+                "solver-linux-aarch64",
+                "solver-linux-x86-64",
+                "solver-win32-x86-64",
+)
+
+for (project in rootProject.children) {
+        val projectName = project.name
+        project.name = "${rootProject.name}-$projectName"
+        project.projectDir = file("subprojects/$projectName")
+}
diff --git a/z3/subprojects/solver-darwin-aarch64/build.gradle.kts b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts
new file mode 100644
index 00000000..21c9739c
--- /dev/null
+++ b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-arm64-osx-11.0"
+val library = "z3java-darwin-aarch64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-darwin-x86-64/build.gradle.kts b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts
new file mode 100644
index 00000000..75e59267
--- /dev/null
+++ b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-osx-10.16"
+val library = "z3java-darwin-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-linux-aarch64/build.gradle.kts b/z3/subprojects/solver-linux-aarch64/build.gradle.kts
new file mode 100644
index 00000000..a8e7e259
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/build.gradle.kts
@@ -0,0 +1,14 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+tasks.jar {
+        // License information is redundant here, since it already gets added to the POM.
+        exclude("**/*.license")
+}
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so
new file mode 100755
index 00000000..f7013e4f
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license
new file mode 100644
index 00000000..6f1e5a96
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license
@@ -0,0 +1,6 @@
+Copyright (c) Microsoft Corporations
+
+SPDX-License-Identifier: MIT
+
+This file was created from the Z3 4.12.2 release sources using the
+z3/docker/cross_build.sh script in this repository.
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so
new file mode 100755
index 00000000..e37c7cdb
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license
new file mode 100644
index 00000000..6f1e5a96
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license
@@ -0,0 +1,6 @@
+Copyright (c) Microsoft Corporations
+
+SPDX-License-Identifier: MIT
+
+This file was created from the Z3 4.12.2 release sources using the
+z3/docker/cross_build.sh script in this repository.
diff --git a/z3/subprojects/solver-linux-x86-64/build.gradle.kts b/z3/subprojects/solver-linux-x86-64/build.gradle.kts
new file mode 100644
index 00000000..89c737b6
--- /dev/null
+++ b/z3/subprojects/solver-linux-x86-64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-glibc-2.31"
+val library = "z3java-linux-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-win32-x86-64/build.gradle.kts b/z3/subprojects/solver-win32-x86-64/build.gradle.kts
new file mode 100644
index 00000000..c5fa0421
--- /dev/null
+++ b/z3/subprojects/solver-win32-x86-64/build.gradle.kts
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-win"
+val library = "z3java-win32-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.dll")
+                        // Do not include .NET assembly.
+                        exclude("${classifier}/bin/Microsoft.Z3.dll")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver/build.gradle.kts b/z3/subprojects/solver/build.gradle.kts
new file mode 100644
index 00000000..7e898b3e
--- /dev/null
+++ b/z3/subprojects/solver/build.gradle.kts
@@ -0,0 +1,107 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+import tools.refinery.z3.gradle.ClassFilePatcher
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-glibc-2.31"
+val extractedClassesDir = layout.buildDirectory.dir("z3-extracted")
+val extractedSourcesDir = layout.buildDirectory.dir("z3-sources")
+
+java {
+        withJavadocJar()
+        withSourcesJar()
+}
+
+val z3Source: Configuration by configurations.creating {
+        isCanBeConsumed = false
+        isCanBeResolved = true
+}
+
+val extractZ3Jar by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                val jarFile = zipTree(zipFile).matching {
+                        include("${classifier}/bin/com.microsoft.z3.jar")
+                }.singleFile
+                zipTree(jarFile).matching {
+                        exclude("META-INF/MANIFEST.MF")
+                        includeEmptyDirs = false
+                }
+        })
+        into(extractedClassesDir)
+        doLast {
+                // The class initializer off {@see com.microsoft.z3.Native} will try to load the Z3 native libraries
+                // from the system default library path unless the {@code z3.skipLibraryLoad} system property is set.
+                // Since we don't control the library path or system properties, we remove the class initializer entirely.
+                val nativeClassFile = extractedClassesDir.get().file("com/microsoft/z3/Native.class").asFile
+                ClassFilePatcher.removeClassInitializer(nativeClassFile)
+        }
+}
+
+val extractZ3Source by tasks.registering(Sync::class) {
+        dependsOn(z3Source)
+        from({
+                val zipFile = z3Source.singleFile
+                zipTree(zipFile).matching {
+                        include("z3-z3-${version}/src/api/java/**/*")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(4).toTypedArray()
+                relativePath = RelativePath(true, "com", "microsoft", "z3", *pathInBin)
+        }
+        into(extractedSourcesDir)
+}
+
+tasks.jar {
+        // Add class files to our jar manually.
+        from(extractZ3Jar)
+}
+
+tasks.test {
+        useJUnitPlatform()
+}
+
+tasks.named<Jar>("sourcesJar") {
+        from(extractZ3Source)
+}
+
+tasks.named<Javadoc>("javadoc") {
+        source(sourceSets.main.map { it.allJava })
+        source(fileTree(extractedSourcesDir) {
+                builtBy(extractZ3Source)
+                include("**/*.java")
+        })
+        options {
+                this as StandardJavadocDocletOptions
+                addBooleanOption("Xdoclint:none", true)
+                // {@code -Xmaxwarns 0} will print all warnings, so we must keep at least one.
+                addStringOption("Xmaxwarns", "1")
+                quiet()
+        }
+}
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+        z3Source("Z3Prover:z3:${version}@zip")
+        // This dependency doesn't get added to Maven metadata, so we have to add the class files to our jar manually.
+        api(files(extractZ3Jar))
+        implementation(libs.jna)
+        implementation(project(":refinery-z3-solver-darwin-aarch64"))
+        implementation(project(":refinery-z3-solver-darwin-x86-64"))
+        implementation(project(":refinery-z3-solver-linux-aarch64"))
+        implementation(project(":refinery-z3-solver-linux-x86-64"))
+        implementation(project(":refinery-z3-solver-win32-x86-64"))
+        testImplementation(libs.junit.api)
+        testRuntimeOnly(libs.junit.engine)
+        testRuntimeOnly("org.junit.platform:junit-platform-launcher")
+}
diff --git a/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java
new file mode 100644
index 00000000..84f99540
--- /dev/null
+++ b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java
@@ -0,0 +1,154 @@
+/*
+ * Copyright 2010-2022 Google LLC
+ * Copyright 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ *
+ * This file is based on
+ * https://github.com/google/or-tools/blob/f3d1d5f6a67356ec38a7fd2ab607624eea8ad3a6/ortools/java/com/google/ortools/Loader.java
+ * We adapted the loader logic to extract the JNI libraries of Z3 and the corresponding dependencies instead of the
+ * Google OR-Tools JNI libraries.
+ */
+package tools.refinery.z3;
+
+import com.sun.jna.Platform;
+
+import java.io.IOException;
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.nio.file.*;
+import java.nio.file.attribute.BasicFileAttributes;
+import java.util.Map;
+
+public final class Z3SolverLoader {
+        private static final String JNI_LIBRARY_NAME = "z3java";
+        private static final String SOLVER_LIBRARY_NAME = "z3";
+
+        private static boolean loaded;
+
+        private Z3SolverLoader() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static synchronized void loadNativeLibraries() {
+                if (loaded) {
+                        return;
+                }
+                try {
+                        System.loadLibrary(getOsSpecificLibraryName(JNI_LIBRARY_NAME));
+                        loaded = true;
+                        return;
+                } catch (UnsatisfiedLinkError e) {
+                        // Continue, we'll have to extract the libraries from the classpath.
+                }
+                try {
+                        extractAndLoad();
+                        loaded = true;
+                } catch (IOException e) {
+                        throw new IllegalStateException("Could not extract and load " + JNI_LIBRARY_NAME, e);
+                }
+        }
+
+        private static void extractAndLoad() throws IOException {
+                var resourceName = JNI_LIBRARY_NAME + "-" + Platform.RESOURCE_PREFIX;
+                var resource = Z3SolverLoader.class.getClassLoader().getResource(resourceName);
+                if (resource == null) {
+                        throw new IllegalStateException("Resource %s was not found".formatted(resourceName));
+                }
+                URI resourceUri;
+                try {
+                        resourceUri = resource.toURI();
+                } catch (URISyntaxException e) {
+                        throw new IllegalStateException("Invalid resource URI: " + resource);
+                }
+                FileSystem fileSystem = null;
+                boolean newFileSystem = false;
+                Path extractedPath;
+                try {
+                        try {
+                                fileSystem = FileSystems.newFileSystem(resourceUri, Map.of());
+                                newFileSystem = true;
+                        } catch (FileSystemAlreadyExistsException e) {
+                                fileSystem = FileSystems.getFileSystem(resourceUri);
+                        }
+                        var resourcePath = fileSystem.provider().getPath(resourceUri);
+                        if (fileSystem.equals(FileSystems.getDefault())) {
+                                extractedPath = resourcePath;
+                        } else {
+                                extractedPath = extract(resourcePath);
+                        }
+                } finally {
+                        if (newFileSystem) {
+                                fileSystem.close();
+                        }
+                }
+                // We can't rely on RPATH, so we load libraries in reverse dependency order manually.
+                try {
+                        loadFromPath(extractedPath, SOLVER_LIBRARY_NAME);
+                } catch (UnsatisfiedLinkError e) {
+                        if (Platform.isWindows()) {
+                                // Try again with our packaged msvcp140 if the system one is missing.
+                                loadFromPathExactName(extractedPath, "vcruntime140.dll");
+                                loadFromPathExactName(extractedPath, "vcruntime140_1.dll");
+                                loadFromPathExactName(extractedPath, "msvcp140.dll");
+                                loadFromPath(extractedPath, SOLVER_LIBRARY_NAME);
+                        } else {
+                                throw e;
+                        }
+                }
+                loadFromPath(extractedPath, JNI_LIBRARY_NAME);
+        }
+
+        private static Path extract(Path resourcePath) throws IOException {
+                var tempDir = Files.createTempDirectory(JNI_LIBRARY_NAME).toAbsolutePath();
+                tempDir.toFile().deleteOnExit();
+                Files.walkFileTree(resourcePath, new SimpleFileVisitor<>() {
+                        @Override
+                        public FileVisitResult preVisitDirectory(Path dir, BasicFileAttributes attrs) throws IOException {
+                                var result = super.preVisitDirectory(dir, attrs);
+                                var targetPath = getTargetPath(dir, resourcePath, tempDir);
+                                if (!Files.exists(targetPath)) {
+                                        Files.createDirectory(targetPath);
+                                        targetPath.toFile().deleteOnExit();
+                                }
+                                return result;
+                        }
+
+                        @Override
+                        public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException {
+                                var result = super.visitFile(file, attrs);
+                                var targetPath = getTargetPath(file, resourcePath, tempDir);
+                                Files.copy(file, targetPath);
+                                targetPath.toFile().deleteOnExit();
+                                return result;
+                        }
+                });
+                return tempDir;
+        }
+
+        private static Path getTargetPath(Path sourcePath, Path resourcePath, Path tempDir) {
+                var targetPath = tempDir.resolve(resourcePath.relativize(sourcePath).toString()).normalize();
+                if (!targetPath.startsWith(tempDir)) {
+                        throw new IllegalStateException("Target path '%s' for '%s' is outside '%s'"
+                                        .formatted(targetPath, sourcePath, tempDir));
+                }
+                return targetPath;
+        }
+
+        private static String getOsSpecificLibraryName(String libraryName) {
+                var osSpecificLibraryNamePrefix = Platform.isWindows() ? "lib" : "";
+                return osSpecificLibraryNamePrefix + libraryName;
+        }
+
+        private static void loadFromPath(Path extractedPath, String libraryName) {
+                var osSpecificLibraryName = getOsSpecificLibraryName(libraryName);
+                loadFromPathExactName(extractedPath, System.mapLibraryName(osSpecificLibraryName));
+        }
+
+        private static void loadFromPathExactName(Path extractedPath, String exactName) {
+                var library = extractedPath.resolve(exactName)
+                                .toAbsolutePath()
+                                .toString();
+                System.load(library);
+        }
+}
diff --git a/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java
new file mode 100644
index 00000000..df3139cc
--- /dev/null
+++ b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+package tools.refinery.z3;
+
+import com.microsoft.z3.*;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+class Z3SolverLoaderTest {
+        @Test
+        void testLoad() {
+                assertDoesNotThrow(Z3SolverLoader::loadNativeLibraries);
+                try (var context = new Context()) {
+                        var solver = context.mkSolver();
+                        var a = context.mkConst("a", context.getIntSort());
+                        var b = context.mkConst("b", context.getIntSort());
+                        solver.add(context.mkEq(a, context.mkInt(3)));
+                        solver.add(context.mkEq(b, context.mkMul(context.mkInt(2), a)));
+                        assertEquals(Status.SATISFIABLE, solver.check());
+                        var model = solver.getModel();
+                        var bValue = (IntNum) model.getConstInterp(b);
+                        assertEquals(6, bValue.getInt());
+                }
+        }
+}