Fetch Z3 distribution during build

.github/workflows/gradle.yml

@@ -51,6 +51,10 @@ jobs:
         path: |
           symbolic-executor/lib/symbolic-executor.jar
           build/svcomp-runtime/java-smt-latest.jar
+          libs/java-library-path/com.microsoft.z3.jar
+          libs/java-library-path/libz3.so
+          libs/java-library-path/libz3java.so
+          libs/java-library-path/libz3.a
         if-no-files-found: error
         retention-days: 1
 
@@ -85,6 +89,11 @@ jobs:
         mkdir -p libs/java-library-path
         cp "${RUNNER_TEMP}/release-jars/build/svcomp-runtime/java-smt-latest.jar" \
           libs/java-library-path/java-smt-latest.jar
+        cp "${RUNNER_TEMP}/release-jars/libs/java-library-path/com.microsoft.z3.jar" \
+          "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3.so" \
+          "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3java.so" \
+          "${RUNNER_TEMP}/release-jars/libs/java-library-path/libz3.a" \
+          libs/java-library-path/
     - name: Download WitnessCreator runtime
       run: |
         version="${WITNESS_CREATOR_VERSION}"

build.gradle

@@ -4,56 +4,82 @@ plugins {
     id 'com.diffplug.spotless' version '6.9.0'
 }
 
-tasks.register('copyNativeLibs', Copy) { // copies correct native z3 files to libs/
-        def osArchMap = [
-                'windows-x64': 'z3-4.15.4-x64-win',
-                'windows-x86': 'z3-4.15.4-x86-win',
-                'osx-x64'    : 'z3-4.15.4-x64-osx-13.7.6',
-                'osx-arm64'  : 'z3-4.15.4-arm64-osx-13.7.6',
-                'linux-x64'  : 'z3-4.15.4-x64-glibc-2.39',
-                'linux-arm64': 'z3-4.15.4-arm64-glibc-2.34'
-        ]
-
-        def os = OperatingSystem.current()
-        println("Operating system: $os")
-
-        def arch = System.getProperty("os.arch") // Use Java system property to get architecture
-        println("Architecture: $arch")
-
-
-    def osKey = ''
-        switch (os) {
-            case OperatingSystem.LINUX:
-                osKey = arch == "aarch64" ? "linux-arm64" : "linux-x64"
-                break;
-            case OperatingSystem.MAC_OS:
-                osKey = arch == "aarch64" ? "osx-arm64" : "osx-x64"
-                break;
-            case OperatingSystem.WINDOWS:
-                osKey = arch == "x86" ? "windows-x86" : "windows-x64"
-                break;
-        }
-        println("Operating system key: $osKey")
-        if (!osKey) {
-            throw new GradleException("Unsupported operating system or architecture.")
-        }
+ext {
+    z3Version = libs.versions.z3.get()
+    z3NativeDir = layout.projectDirectory.dir('libs/java-library-path')
+}
+
+def z3Platform() {
+    def os = OperatingSystem.current()
+    def arch = System.getProperty('os.arch').toLowerCase(Locale.ROOT)
+    def z3Arch = arch in ['aarch64', 'arm64'] ? 'arm64' : 'x64'
+
+    if (os.isLinux()) {
+        def libc = z3Arch == 'arm64' ? 'glibc-2.34' : 'glibc-2.39'
+        return [distribution: "z3-${z3Version}-${z3Arch}-${libc}"]
+    }
+    if (os.isMacOsX()) {
+        return [distribution: "z3-${z3Version}-${z3Arch}-osx-13.7.6"]
+    }
+    if (os.isWindows()) {
+        def windowsArch = arch in ['x86', 'i386'] ? 'x86' : z3Arch
+        return [distribution: "z3-${z3Version}-${windowsArch}-win"]
+    }
+
+    throw new GradleException("Unsupported operating system for Z3 native libraries: ${os}")
+}
+
+configurations {
+    cfgExtractor
+}
+
+dependencies {
+    cfgExtractor 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT'
+}
+
+def z3Platform = z3Platform()
+def z3Archive = layout.buildDirectory.file("z3/${z3Platform.distribution}.zip")
+def z3DownloadUrl = "https://github.com/Z3Prover/z3/releases/download/z3-${z3Version}/${z3Platform.distribution}.zip"
 
-        def z3Zip = file("libs/${osArchMap[osKey]}.zip")
-        if (!z3Zip.exists()) {
-            throw new GradleException("Z3 distribution zip file not found at ${z3Zip.path}")
+tasks.register('downloadZ3Distribution') {
+    description = 'Downloads the official Z3 distribution for the current platform.'
+    inputs.property 'url', z3DownloadUrl
+    outputs.file z3Archive
+
+    doLast {
+        def archive = z3Archive.get().asFile
+        def temporaryArchive = new File(archive.parentFile, "${archive.name}.part")
+        archive.parentFile.mkdirs()
+
+        new URL(z3DownloadUrl).withInputStream { input ->
+            temporaryArchive.withOutputStream { output -> output << input }
         }
-            from zipTree(z3Zip)
-            into 'libs/java-library-path'
-            include "${osArchMap[osKey]}/bin/z3*"
-            include "${osArchMap[osKey]}/bin/libz3.*"
-            include "${osArchMap[osKey]}/bin/libz3java.*"
-            include "${osArchMap[osKey]}/bin/com.microsoft.z3.jar"
-            eachFile { FileCopyDetails fcp ->
-                fcp.relativePath = new RelativePath(true, fcp.name)
-            }
-            includeEmptyDirs false
+        java.nio.file.Files.move(
+                temporaryArchive.toPath(),
+                archive.toPath(),
+                java.nio.file.StandardCopyOption.REPLACE_EXISTING
+        )
+    }
+}
+
+tasks.register('copyNativeLibs', Sync) {
+    description = 'Fetches the Z3 Java bindings and native libraries.'
+    dependsOn tasks.named('downloadZ3Distribution')
+    inputs.property 'runtimeLayoutVersion', 2
 
+    into z3NativeDir
+    duplicatesStrategy = DuplicatesStrategy.EXCLUDE
+
+    from({ zipTree(z3Archive.get().asFile) }) {
+        include "${z3Platform.distribution}/bin/libz3.*"
+        include "${z3Platform.distribution}/bin/libz3java.*"
+        include "${z3Platform.distribution}/bin/com.microsoft.z3.jar"
+        eachFile { details ->
+            details.relativePath = new RelativePath(true, details.name)
+        }
+        includeEmptyDirs = false
     }
+}
 tasks.register('downloadJacoco') {
     description = 'Downloads JaCoCo agent jar for coverage collection'
     def jacocoVersion = '0.8.13'
@@ -85,14 +111,6 @@ tasks.register('downloadJacoco') {
     }
 }
 
-configurations {
-    cfgExtractor
-}
-
-dependencies {
-    cfgExtractor 'de.uzl.its:cfg-extractor:1.0-SNAPSHOT'
-}
-
 tasks.register('downloadCfgExtractor', Copy) {
     description = 'Downloads cfg-extractor fat JAR from GitHub Packages'
     from configurations.cfgExtractor

docker/Dockerfile

@@ -2,18 +2,15 @@ FROM gradle:8.13.0-jdk17
 
 # Install Python and other tools
 RUN apt-get update && \
-    apt-get install -y python3 python3-pip python3-venv findutils unzip ant
+    apt-get install -y python3 python3-pip python3-venv findutils unzip
 
 # Set working dir
 WORKDIR /app
 
 # Copy project source
 COPY . .
 
-RUN chmod +x ./scripts/build-javasmt.sh
-RUN ./scripts/build-javasmt.sh
-
-# Copy native Z3 libs via Gradle task (assumes they go to /app/libs/java-library-path)
+# Fetch native Z3 libs via Gradle task
 RUN gradle copyNativeLibs
 
 # Build Java code (skip tests)
@@ -24,4 +21,4 @@ RUN gradle clean build -x test
 RUN cp /app/libs/java-library-path/libz3*.so /usr/lib/
 
 # Set Z3 JAR in CLASSPATH so it's visible to javaagent (NO JVM FLAGS NEEDED)
-ENV CLASSPATH=/app/libs/java-library-path/com.microsoft.z3.jar
+ENV CLASSPATH=/app/libs/java-library-path/com.microsoft.z3.jar

scripts/package-svcomp.sh

@@ -23,7 +23,7 @@ set -euo pipefail
 #
 # - .venv_ubuntu_24_04_1__x86_64/
 #
-# Z3 and JavaSMT are taken from the vendored files in this repository.
+# Z3 and JavaSMT are taken from the runtime files prepared by CI.
 #
 ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
 cd "$ROOT_DIR"
@@ -41,8 +41,6 @@ ARTIFACT_DIR="$(cd "${SWAT_SVCOMP_ARTIFACT_DIR:-$ROOT_DIR}" && pwd)"
 RUNTIME_DIR="${SWAT_SVCOMP_RUNTIME_DIR:-${SWAT_SVCOMP_REFERENCE_DIR:-}}"
 WITNESS_CREATOR_DIR="${SWAT_SVCOMP_WITNESS_CREATOR_DIR:-}"
 VENV_DIR_NAME="${SWAT_SVCOMP_VENV_DIR_NAME:-.venv_ubuntu_24_04_1__x86_64}"
-LINUX_Z3_DIST="z3-4.15.4-x64-glibc-2.39"
-LINUX_Z3_ZIP="${ROOT_DIR}/libs/${LINUX_Z3_DIST}.zip"
 JAVA_SMT_JAR="${ROOT_DIR}/libs/java-library-path/java-smt-latest.jar"
 
 if [[ -n "$RUNTIME_DIR" ]]; then
@@ -106,12 +104,11 @@ copy_artifact_tree() {
 install_z3_runtime_file() {
   local name="$1"
   local mode="${2:-0644}"
+  local src="${ROOT_DIR}/libs/java-library-path/${name}"
   local dest="${PACKAGE_DIR}/libs/java-library-path/${name}"
 
-  [[ -f "$LINUX_Z3_ZIP" ]] || fail "missing vendored Linux Z3 distribution: ${LINUX_Z3_ZIP}"
-  mkdir -p "$(dirname "$dest")"
-  unzip -p "$LINUX_Z3_ZIP" "${LINUX_Z3_DIST}/bin/${name}" > "$dest"
-  chmod "$mode" "$dest"
+  [[ -f "$src" ]] || fail "missing prepared Z3 runtime file: ${src}"
+  copy_artifact_file "$src" "$dest" "$mode"
 }
 
 echo "Packaging repository files from: ${ROOT_DIR}"
@@ -149,7 +146,6 @@ copy_tree_files symbolic-explorer "$PACKAGE_DIR/symbolic-explorer"
 [[ -f "$WITNESS_CREATOR_DIR/witnesses/witness.st" ]] || fail "missing WitnessCreator template: ${WITNESS_CREATOR_DIR}/witnesses/witness.st"
 copy_artifact_tree "$WITNESS_CREATOR_DIR" "$PACKAGE_DIR/WitnessCreator"
 
-install_z3_runtime_file z3 0755
 install_z3_runtime_file libz3.so
 install_z3_runtime_file libz3java.so
 install_z3_runtime_file com.microsoft.z3.jar

settings.gradle

@@ -61,12 +61,14 @@ dependencyResolutionManagement {
     versionCatalogs {
         libs {
             version('asm','9.6')
+            version('z3', '4.15.4')
             library('asm-core', 'org.ow2.asm','asm').versionRef('asm')
             library('asm-commons', 'org.ow2.asm','asm-commons').versionRef('asm')
             library('asm-util', 'org.ow2.asm','asm-util').versionRef('asm')
             library('asm-tree', 'org.ow2.asm','asm-tree').versionRef('asm')
             library('jackson-databind', 'com.fasterxml.jackson.core:jackson-databind:2.14.1')
             library('java-smt', 'org.sosy-lab:java-smt:6.0.0')
+            library('javasmt-solver-z3', 'org.sosy-lab', 'javasmt-solver-z3').versionRef('z3')
             library('spock-core', 'org.spockframework:spock-core:2.2-groovy-4.0')
             library('mockito-core', 'org.mockito:mockito-core:3.12.4')
             library('logback-classic', 'ch.qos.logback:logback-classic:1.5.3')

symbolic-executor/build.gradle

@@ -38,16 +38,28 @@ dependencies {
     implementation libs.bundles.asm
     implementation libs.jackson.databind
     implementation libs.java.smt
-
-    implementation rootProject.fileTree(dir: 'libs/java-library-path', include: ['*.jar']) // loads com.microsoft.z3 and java-smt
+    implementation libs.javasmt.solver.z3
 
     testImplementation libs.spock.core
     testImplementation libs.jackson.databind
     testImplementation libs.mockito.core
 }
 
 test {
-    systemProperty "java.library.path", "../libs/java-library-path"
+    dependsOn rootProject.tasks.named('copyNativeLibs')
+    def z3NativePath = rootProject.z3NativeDir.asFile.absolutePath
+    def currentOs = org.gradle.internal.os.OperatingSystem.current()
+    systemProperty "java.library.path", z3NativePath
+    if (currentOs.isLinux()) {
+        def existingPath = System.getenv('LD_LIBRARY_PATH')
+        environment "LD_LIBRARY_PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath
+    } else if (currentOs.isMacOsX()) {
+        def existingPath = System.getenv('DYLD_LIBRARY_PATH')
+        environment "DYLD_LIBRARY_PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath
+    } else if (currentOs.isWindows()) {
+        def existingPath = System.getenv('PATH')
+        environment "PATH", existingPath ? "${z3NativePath}${File.pathSeparator}${existingPath}" : z3NativePath
+    }
     // Surface SWAT errors as exceptions instead of halting the test JVM
     systemProperty "exitOnError", "false"