Upgrade z3 to 4.13.4 (#167)

* Upgrade z3 to 4.13.4

* Upgrade ksmt version to 0.5.27

README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.26)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.27)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.26")
+implementation("io.ksmt:ksmt-core:0.5.27")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.26")
+implementation("io.ksmt:ksmt-z3:0.5.27")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.26"
+version = "0.5.27"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.26")    
+    implementation("io.ksmt:ksmt-core:0.5.27")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.26")
+    implementation("io.ksmt:ksmt-z3:0.5.27")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.26")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.27")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.26")
+    implementation("io.ksmt:ksmt-core:0.5.27")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.26")
+    implementation("io.ksmt:ksmt-z3:0.5.27")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.26")
+    implementation("io.ksmt:ksmt-runner:0.5.27")
 }
 
 java {

ksmt-runner/src/test/kotlin/io/ksmt/solver/runner/SolverRunnerTest.kt

@@ -1,21 +1,19 @@
 package io.ksmt.solver.runner
 
-import org.junit.jupiter.api.AfterAll
-import org.junit.jupiter.api.AfterEach
-import org.junit.jupiter.api.BeforeAll
-import org.junit.jupiter.api.BeforeEach
 import io.ksmt.KContext
 import io.ksmt.runner.generated.createInstance
 import io.ksmt.runner.generated.models.SolverType
 import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverStatus
 import io.ksmt.solver.z3.KZ3Solver
 import io.ksmt.solver.z3.KZ3SolverConfiguration
-import io.ksmt.utils.getValue
 import io.ksmt.utils.mkConst
+import org.junit.jupiter.api.AfterAll
+import org.junit.jupiter.api.AfterEach
+import org.junit.jupiter.api.BeforeAll
+import org.junit.jupiter.api.BeforeEach
 import kotlin.test.Test
 import kotlin.test.assertEquals
-import kotlin.test.assertNotEquals
 import kotlin.test.assertTrue
 import kotlin.time.Duration.Companion.milliseconds
 
@@ -126,33 +124,6 @@ class SolverRunnerTest {
         assertTrue("timeout" in solver.reasonOfUnknown())
     }
 
-    @Test
-    fun testSolverConfiguration(): Unit = with(context) {
-        val i by intSort
-        val j by intSort
-
-        val expr = (i gt j) or (i lt j)
-        solver.assert(expr)
-
-        solver.configure { setZ3Option("random_seed", 17) }
-        val status1 = solver.check()
-        assertEquals(KSolverStatus.SAT, status1)
-        val model1 = solver.model()
-
-        solver.configure { setZ3Option("random_seed", 42) }
-        val status2 = solver.check()
-        assertEquals(KSolverStatus.SAT, status2)
-        val model2 = solver.model()
-
-        solver.configure { setZ3Option("random_seed", 17) }
-        val status3 = solver.check()
-        assertEquals(KSolverStatus.SAT, status3)
-        val model3 = solver.model()
-
-        assertNotEquals(model1, model2)
-        assertEquals(model1, model3)
-    }
-
     @Test
     fun testBulkAssert(): Unit = with(context) {
         val a = boolSort.mkConst("a")

ksmt-z3/ksmt-z3-core/build.gradle.kts

@@ -9,7 +9,7 @@ repositories {
     mavenCentral()
 }
 
-val z3Version = "4.13.0"
+val z3Version = "4.13.4"
 
 val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", listOf("**/com.microsoft.z3.jar")) }
 

ksmt-z3/ksmt-z3-native/build.gradle.kts

@@ -19,7 +19,7 @@ val `mac-arm` by sourceSets.creating
 val `windows-arm` by sourceSets.creating
 val `linux-arm` by sourceSets.creating
 
-val z3Version = "4.13.0"
+val z3Version = "4.13.4"
 
 val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll")
 val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so")
@@ -28,9 +28,9 @@ 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-11.7.10", macDylibPath), null),
-    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", macDylibPath), null),
-    Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.35", linuxSoPath), null),
+    Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.7.1", macDylibPath), null),
+    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.7.1", macDylibPath), null),
+    Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.34", linuxSoPath), null),
 )
 
 z3Binaries.forEach { it.first.compileClasspath = compileConfig }