From 525190311c4eb31d1864c0a3612b279861eac959 Mon Sep 17 00:00:00 2001 From: tochilinak Date: Mon, 6 Apr 2026 18:21:39 +0300 Subject: [PATCH 1/4] Updated Z3 --- ksmt-z3/ksmt-z3-native/build.gradle.kts | 33 ++++++++----------------- 1 file changed, 10 insertions(+), 23 deletions(-) diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index 89306c80d..826eac709 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-native/build.gradle.kts @@ -4,15 +4,11 @@ plugins { id("io.ksmt.ksmt-base") } -val distDir = projectDir.parentFile.resolve("dist") - repositories { mavenCentral() - flatDir { dirs(distDir) } } val compileConfig by configurations.creating -val z3NativeLinuxX64 by configurations.creating val `windows-x64` by sourceSets.creating val `linux-x64` by sourceSets.creating @@ -21,18 +17,18 @@ val `mac-arm` by sourceSets.creating val `windows-arm` by sourceSets.creating val `linux-arm` by sourceSets.creating -val z3Version = "4.15.3" +val z3Version = "4.16.0" val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll") val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so") val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib") val z3Binaries = listOf( - Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null), - Triple(`linux-x64`, null, z3NativeLinuxX64), - Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.7.6", macDylibPath), null), - Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.7.6", macDylibPath), null), - Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.34", linuxSoPath), null), + Pair(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath)), + Pair(`linux-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-glibc-2.39", linuxSoPath)), + Pair(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-15.7.3", macDylibPath)), + Pair(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-15.7.3", macDylibPath)), + Pair(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.38", linuxSoPath)), ) z3Binaries.forEach { it.first.compileClasspath = compileConfig } @@ -40,11 +36,9 @@ z3Binaries.forEach { it.first.compileClasspath = compileConfig } dependencies { compileConfig(project(":ksmt-core")) compileConfig(project(":ksmt-z3:ksmt-z3-core")) - - z3NativeLinuxX64("z3", "z3-native-linux-x86-64", z3Version, ext = "zip") } -z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) -> +z3Binaries.forEach { (sourceSet, z3BinaryTask) -> val name = sourceSet.name val artifactName = "ksmt-z3-native-$name" val systemArch = name.replace('-', '/') @@ -57,14 +51,10 @@ z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) -> archiveBaseName.set(artifactName) from(sourceSet.output) - z3BinaryTask?.let { + z3BinaryTask.let { dependsOn(it) from(it.outputFiles) { into("lib/$systemArch/z3") } } - - nativeConfig?.let { - copyArtifactsIntoJar(it, this, "lib/$systemArch/z3") - } } publishing.publications { @@ -81,17 +71,14 @@ z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) -> } tasks.getByName("jar") { - z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) -> + z3Binaries.forEach { (sourceSet, z3BinaryTask) -> from(sourceSet.output) val systemArch = sourceSet.name.replace('-', '/') - z3BinaryTask?.let { + z3BinaryTask.let { dependsOn(it) from(it.outputFiles) { into("lib/$systemArch/z3") } } - nativeConfig?.let { - copyArtifactsIntoJar(it, this, "lib/$systemArch/z3") - } } } From 1dff7ee7217cd6c15d2e6f1fee6b0cce7d397a8c Mon Sep 17 00:00:00 2001 From: Ekaterina Tochilina Date: Mon, 6 Apr 2026 18:30:50 +0300 Subject: [PATCH 2/4] Updated Ubuntu on CI --- .github/workflows/build-and-run-tests.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index 9df103bba..def962558 100644 --- a/.github/workflows/build-and-run-tests.yml +++ b/.github/workflows/build-and-run-tests.yml @@ -15,7 +15,7 @@ jobs: name: Run tests strategy: matrix: - os: [ ubuntu-22.04, windows-latest, macos-latest ] + os: [ ubuntu-24.04, windows-latest, macos-latest ] runs-on: ${{ matrix.os }} From e9bdace2980f11cdfddc7e72daa4ee85f8800c8a Mon Sep 17 00:00:00 2001 From: Ekaterina Tochilina Date: Mon, 6 Apr 2026 20:09:03 +0300 Subject: [PATCH 3/4] Commented out power test --- .../kotlin/io/ksmt/test/ModelGenerationTest.kt | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt index 32f53ebcb..02c119d7e 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt +++ b/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt @@ -254,15 +254,15 @@ abstract class ModelGenerationTest { op { mkArithGtNoSimplify(it.v(intSort), it.v(intSort)) } op { mkArithLeNoSimplify(it.v(intSort), it.v(intSort)) } op { mkArithLtNoSimplify(it.v(intSort), it.v(intSort)) } - unspecifiedOp { - val base = it.v(intSort) - val power = it.v(intSort) - UnspecifiedOp( - op = mkArithPowerNoSimplify(base, power), - unspecifiedIf = (base eq 0.expr) and (power eq 0.expr), - unspecifiedValue = 0.expr, - ) - } +// unspecifiedOp { +// val base = it.v(intSort) +// val power = it.v(intSort) +// UnspecifiedOp( +// op = mkArithPowerNoSimplify(base, power), +// unspecifiedIf = (base eq 0.expr) and (power eq 0.expr), +// unspecifiedValue = 0.expr, +// ) +// } op { mkArithUnaryMinusNoSimplify(it.v(intSort)) } unspecifiedOp { From 5974c688a7960faebcfd6e4da6862bf83aea4538 Mon Sep 17 00:00:00 2001 From: Ekaterina Tochilina Date: Mon, 6 Apr 2026 21:01:57 +0300 Subject: [PATCH 4/4] Fallback to 4.15.8 --- .../kotlin/io/ksmt/test/ModelGenerationTest.kt | 18 +++++++++--------- ksmt-z3/ksmt-z3-native/build.gradle.kts | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt index 02c119d7e..32f53ebcb 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt +++ b/ksmt-test/src/test/kotlin/io/ksmt/test/ModelGenerationTest.kt @@ -254,15 +254,15 @@ abstract class ModelGenerationTest { op { mkArithGtNoSimplify(it.v(intSort), it.v(intSort)) } op { mkArithLeNoSimplify(it.v(intSort), it.v(intSort)) } op { mkArithLtNoSimplify(it.v(intSort), it.v(intSort)) } -// unspecifiedOp { -// val base = it.v(intSort) -// val power = it.v(intSort) -// UnspecifiedOp( -// op = mkArithPowerNoSimplify(base, power), -// unspecifiedIf = (base eq 0.expr) and (power eq 0.expr), -// unspecifiedValue = 0.expr, -// ) -// } + unspecifiedOp { + val base = it.v(intSort) + val power = it.v(intSort) + UnspecifiedOp( + op = mkArithPowerNoSimplify(base, power), + unspecifiedIf = (base eq 0.expr) and (power eq 0.expr), + unspecifiedValue = 0.expr, + ) + } op { mkArithUnaryMinusNoSimplify(it.v(intSort)) } unspecifiedOp { diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index 826eac709..a5ce9e4d1 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-native/build.gradle.kts @@ -17,7 +17,7 @@ val `mac-arm` by sourceSets.creating val `windows-arm` by sourceSets.creating val `linux-arm` by sourceSets.creating -val z3Version = "4.16.0" +val z3Version = "4.15.8" val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll") val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so")