Skip to content

Commit 3649c3a

Browse files
SaloedSaloed
authored
Upgrade z3 to 4.13.4 (#167)
* Upgrade z3 to 4.13.4 * Upgrade ksmt version to 0.5.27
1 parent 957ead4 commit 3649c3a

File tree

8 files changed

+19
-48
lines changed

8 files changed

+19
-48
lines changed

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
1111
* Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
1212

1313
[![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)
14-
[![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)
14+
[![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)
1515
[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
1616

1717
## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
2020

2121
```kotlin
2222
// core
23-
implementation("io.ksmt:ksmt-core:0.5.26")
23+
implementation("io.ksmt:ksmt-core:0.5.27")
2424
// z3 solver
25-
implementation("io.ksmt:ksmt-z3:0.5.26")
25+
implementation("io.ksmt:ksmt-z3:0.5.27")
2626
```
2727

2828
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‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ plugins {
1111
}
1212

1313
group = "io.ksmt"
14-
version = "0.5.26"
14+
version = "0.5.27"
1515

1616
repositories {
1717
mavenCentral()

‎docs/getting-started.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ repositories {
3434
```kotlin
3535
dependencies {
3636
// core
37-
implementation("io.ksmt:ksmt-core:0.5.26")
37+
implementation("io.ksmt:ksmt-core:0.5.27")
3838
}
3939
```
4040

@@ -43,9 +43,9 @@ dependencies {
4343
```kotlin
4444
dependencies {
4545
// z3
46-
implementation("io.ksmt:ksmt-z3:0.5.26")
46+
implementation("io.ksmt:ksmt-z3:0.5.27")
4747
// bitwuzla
48-
implementation("io.ksmt:ksmt-bitwuzla:0.5.26")
48+
implementation("io.ksmt:ksmt-bitwuzla:0.5.27")
4949
}
5050
```
5151

‎examples/build.gradle.kts‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ repositories {
99

1010
dependencies {
1111
// core
12-
implementation("io.ksmt:ksmt-core:0.5.26")
12+
implementation("io.ksmt:ksmt-core:0.5.27")
1313
// z3 solver
14-
implementation("io.ksmt:ksmt-z3:0.5.26")
14+
implementation("io.ksmt:ksmt-z3:0.5.27")
1515
// Runner and portfolio solver
16-
implementation("io.ksmt:ksmt-runner:0.5.26")
16+
implementation("io.ksmt:ksmt-runner:0.5.27")
1717
}
1818

1919
java {

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

Lines changed: 4 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,19 @@
11
package io.ksmt.solver.runner
22

3-
import org.junit.jupiter.api.AfterAll
4-
import org.junit.jupiter.api.AfterEach
5-
import org.junit.jupiter.api.BeforeAll
6-
import org.junit.jupiter.api.BeforeEach
73
import io.ksmt.KContext
84
import io.ksmt.runner.generated.createInstance
95
import io.ksmt.runner.generated.models.SolverType
106
import io.ksmt.solver.KSolver
117
import io.ksmt.solver.KSolverStatus
128
import io.ksmt.solver.z3.KZ3Solver
139
import io.ksmt.solver.z3.KZ3SolverConfiguration
14-
import io.ksmt.utils.getValue
1510
import io.ksmt.utils.mkConst
11+
import org.junit.jupiter.api.AfterAll
12+
import org.junit.jupiter.api.AfterEach
13+
import org.junit.jupiter.api.BeforeAll
14+
import org.junit.jupiter.api.BeforeEach
1615
import kotlin.test.Test
1716
import kotlin.test.assertEquals
18-
import kotlin.test.assertNotEquals
1917
import kotlin.test.assertTrue
2018
import kotlin.time.Duration.Companion.milliseconds
2119

@@ -126,33 +124,6 @@ class SolverRunnerTest {
126124
assertTrue("timeout" in solver.reasonOfUnknown())
127125
}
128126

129-
@Test
130-
fun testSolverConfiguration(): Unit = with(context) {
131-
val i by intSort
132-
val j by intSort
133-
134-
val expr = (i gt j) or (i lt j)
135-
solver.assert(expr)
136-
137-
solver.configure { setZ3Option("random_seed", 17) }
138-
val status1 = solver.check()
139-
assertEquals(KSolverStatus.SAT, status1)
140-
val model1 = solver.model()
141-
142-
solver.configure { setZ3Option("random_seed", 42) }
143-
val status2 = solver.check()
144-
assertEquals(KSolverStatus.SAT, status2)
145-
val model2 = solver.model()
146-
147-
solver.configure { setZ3Option("random_seed", 17) }
148-
val status3 = solver.check()
149-
assertEquals(KSolverStatus.SAT, status3)
150-
val model3 = solver.model()
151-
152-
assertNotEquals(model1, model2)
153-
assertEquals(model1, model3)
154-
}
155-
156127
@Test
157128
fun testBulkAssert(): Unit = with(context) {
158129
val a = boolSort.mkConst("a")

ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip renamed to ksmt-z3/dist/z3-native-linux-x86-64-4.13.4.zip

13.3 MB
Binary file not shown.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ repositories {
99
mavenCentral()
1010
}
1111

12-
val z3Version = "4.13.0"
12+
val z3Version = "4.13.4"
1313

1414
val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", listOf("**/com.microsoft.z3.jar")) }
1515

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ val `mac-arm` by sourceSets.creating
1919
val `windows-arm` by sourceSets.creating
2020
val `linux-arm` by sourceSets.creating
2121

22-
val z3Version = "4.13.0"
22+
val z3Version = "4.13.4"
2323

2424
val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll")
2525
val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so")
@@ -28,9 +28,9 @@ val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib")
2828
val z3Binaries = listOf(
2929
Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null),
3030
Triple(`linux-x64`, null, z3NativeLinuxX64),
31-
Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", macDylibPath), null),
32-
Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", macDylibPath), null),
33-
Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.35", linuxSoPath), null),
31+
Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.7.1", macDylibPath), null),
32+
Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.7.1", macDylibPath), null),
33+
Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.34", linuxSoPath), null),
3434
)
3535

3636
z3Binaries.forEach { it.first.compileClasspath = compileConfig }

0 commit comments

Comments
 (0)