Upgrade Z3 to 5.0.0

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.6.4)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.5)
 [![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.6.4")
+implementation("io.ksmt:ksmt-core:0.6.5")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.6.4")
+implementation("io.ksmt:ksmt-z3:0.6.5")
 ```
 
 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.6.4"
+version = "0.6.5"
 
 repositories {
     mavenCentral()

docs/getting-started.md

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

examples/build.gradle.kts

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

ksmt-z3/dist/README.md

@@ -0,0 +1,116 @@
+# Z3 native libraries for linux-x86-64
+
+`z3-native-linux-x86-64-<version>.zip` contains `libz3.so` and `libz3java.so` (at the archive root)
+and is consumed by `ksmt-z3-native` as a `flatDir` dependency.
+
+Unlike every other platform, these libraries are **not** taken from the
+[Z3 GitHub release](https://github.com/Z3Prover/z3/releases). The released `x64-glibc-*` package is
+built against a recent glibc (2.39 for Z3 5.0.0) and does not run on older distributions, including
+the `ubuntu-22.04` CI runner. Instead, we build Z3 ourselves against an old glibc and link the C++
+runtime statically.
+
+Every other platform (`x64-win`, `x64-osx-*`, `arm64-osx-*`, `arm64-glibc-*`) is downloaded from the
+Z3 release by `mkZ3ReleaseDownloadTask`, so only linux-x86-64 needs the procedure below.
+
+## Building
+
+The build runs in an AlmaLinux 8 container: it provides glibc 2.28 (older than any supported
+distribution) together with a C++20 capable toolchain, which Z3 requires since 5.0.0
+(it uses `<format>` and `<span>`, so GCC 13+ is a hard requirement).
+
+```bash
+Z3_VERSION=5.0.0
+
+# Z3 sources
+curl -sL -o z3.tar.gz "https://github.com/Z3Prover/z3/archive/refs/tags/z3-$Z3_VERSION.tar.gz"
+tar xzf z3.tar.gz    # -> z3-z3-$Z3_VERSION
+
+docker run --rm -v "$PWD:/work" -e "Z3_VERSION=$Z3_VERSION" \
+    -e "HOST_UID=$(id -u)" -e "HOST_GID=$(id -g)" almalinux:8 bash /work/build-z3-linux-x86-64.sh
+
+cd z3-linux-dist && zip -X -9 "../z3-native-linux-x86-64-$Z3_VERSION.zip" libz3.so libz3java.so
+```
+
+with `build-z3-linux-x86-64.sh`:
+
+```bash
+#!/bin/bash
+set -euo pipefail
+
+dnf -y install --setopt=install_weak_deps=False \
+    gcc-toolset-14 cmake make java-17-openjdk-devel python3
+
+source /opt/rh/gcc-toolset-14/enable
+export JAVA_HOME=$(dirname $(dirname $(readlink -f $(which javac))))
+
+cd "/work/z3-z3-$Z3_VERSION"
+
+# The CMake build gives libz3 a versioned SONAME (e.g. libz3.so.5.0) and makes libz3java
+# depend on that name, but the distribution ships a flat libz3.so. Drop VERSION/SOVERSION
+# to keep the SONAME equal to the file name.
+python3 - <<'EOF'
+p = 'src/CMakeLists.txt'
+s = open(p).read()
+patched = s.replace("""  VERSION ${Z3_VERSION}
+  SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})""", "  POSITION_INDEPENDENT_CODE ON)")
+assert patched != s, "SOVERSION patch did not apply"
+open(p, 'w').write(patched)
+EOF
+
+cmake -S . -B build-linux \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DZ3_BUILD_JAVA_BINDINGS=TRUE \
+    -DZ3_BUILD_LIBZ3_SHARED=TRUE \
+    -DZ3_BUILD_EXECUTABLE=FALSE \
+    -DZ3_BUILD_TEST_EXECUTABLES=FALSE \
+    -DZ3_INCLUDE_GIT_HASH=FALSE \
+    -DZ3_INCLUDE_GIT_DESCRIBE=FALSE \
+    -DCMAKE_SHARED_LINKER_FLAGS="-static-libstdc++ -static-libgcc -Wl,--exclude-libs,ALL" \
+    -DCMAKE_EXE_LINKER_FLAGS="-static-libstdc++ -static-libgcc -Wl,--exclude-libs,ALL"
+
+cmake --build build-linux --target libz3 z3java -j "$(nproc)"
+
+mkdir -p /work/z3-linux-dist
+cp build-linux/libz3.so build-linux/libz3java.so /work/z3-linux-dist/
+chown -R "$HOST_UID:$HOST_GID" /work/z3-linux-dist "/work/z3-z3-$Z3_VERSION"
+```
+
+### Why these linker flags
+
+* `-static-libstdc++ -static-libgcc` — the resulting libraries must not depend on the libstdc++
+  of the machine that runs ksmt.
+* `-Wl,--exclude-libs,ALL` — **required**. Without it the statically linked libstdc++ symbols stay
+  in the dynamic symbol table (~4500 exported `std::` symbols). They then interpose on the
+  libstdc++ used by the Bitwuzla / cvc5 / Yices native libraries loaded into the same JVM,
+  which crashes the JVM with a SIGSEGV inside `libz3.so`.
+
+## Verifying the result
+
+Run these checks before committing a new archive — a mistake here produces libraries that either
+crash at runtime or silently keep the previous Z3 version.
+
+```bash
+cd z3-linux-dist
+
+# 1. The version is the one we intended to build
+strings -a libz3.so | grep -m1 -E '^[0-9]+\.[0-9]+\.[0-9]+\.[0-9]+$'
+
+# 2. No dependency on the system C++ runtime (expect 0)
+objdump -T libz3.so libz3java.so | grep -c GLIBCXX
+
+# 3. Old glibc is enough (expect something well below the oldest supported distribution)
+objdump -T libz3.so libz3java.so | grep -o 'GLIBC_[0-9.]*' | sort -uV | tail -1
+
+# 4. The static C++ runtime is not exported (expect ~90, not ~4500)
+nm -D --defined-only -C libz3.so | grep -c 'std::'
+
+# 5. SONAMEs match the file names, and libz3java depends on plain libz3.so
+objdump -p libz3.so     | grep -E 'SONAME|NEEDED'
+objdump -p libz3java.so | grep -E 'SONAME|NEEDED'
+```
+
+For Z3 5.0.0 this gives: version `5.0.0.0`, `0` GLIBCXX references, max `GLIBC_2.26`,
+`91` exported `std::` symbols, `SONAME libz3.so` / `SONAME libz3java.so`.
+
+Finally run the tests, including `:ksmt-test:test`, which loads several solvers into a single JVM
+and is what catches the symbol interposition problem described above.

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

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

ksmt-z3/ksmt-z3-core/src/main/kotlin/com/microsoft/z3/Util.kt

@@ -1,5 +1,6 @@
 package com.microsoft.z3
 
+import com.microsoft.z3.Native.BoolPtr
 import com.microsoft.z3.Native.IntPtr
 import com.microsoft.z3.Native.LongPtr
 import com.microsoft.z3.enumerations.Z3_error_code
@@ -30,9 +31,9 @@ fun fpExponentInt64OrNull(ctx: Long, expr: Long, biased: Boolean): Long? {
 }
 
 fun fpSignOrNull(ctx: Long, expr: Long): Boolean? {
-    val result = IntPtr()
+    val result = BoolPtr()
     if (!Native.fpaGetNumeralSign(ctx, expr, result)) return null
-    return result.value != 0
+    return result.value
 }
 
 @Suppress("LongParameterList")

ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Model.kt

@@ -13,13 +13,16 @@ import io.ksmt.KContext
 import io.ksmt.decl.KDecl
 import io.ksmt.expr.KExpr
 import io.ksmt.expr.KUninterpretedSortValue
+import io.ksmt.expr.rewrite.simplify.castRealValue
+import io.ksmt.expr.rewrite.simplify.toRealValue
 import io.ksmt.solver.KModel
 import io.ksmt.solver.model.KFuncInterp
 import io.ksmt.solver.model.KFuncInterpEntryVarsFree
 import io.ksmt.solver.model.KFuncInterpEntryWithVars
 import io.ksmt.solver.model.KFuncInterpVarsFree
 import io.ksmt.solver.model.KFuncInterpWithVars
 import io.ksmt.solver.model.KModelImpl
+import io.ksmt.sort.KArithSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KUninterpretedSort
 import io.ksmt.utils.mkFreshConst
@@ -92,7 +95,26 @@ open class KZ3Model(
 
         z3Ctx.releaseTemporaryAst(z3Result)
 
-        return result
+        return result.castToSort(expr.sort)
+    }
+
+    /**
+     * Z3 may assign an arith sort to an expression which differs from the sort ksmt uses.
+     * For example, `(^ a b)` is Real sorted in Z3 even when both `a` and `b` are Int sorted,
+     * while in ksmt this expression is Int sorted.
+     * Because of this, the value we get from a Z3 model may have an unexpected arith sort.
+     *
+     * Cast such values back to the sort of the evaluated expression to keep [eval] sort preserving.
+     * The cast is performed in the same way as in the ksmt expression simplifier
+     * (see [castRealValue]) and therefore the value we produce here is consistent
+     * with the value produced by a detached model.
+     * */
+    private fun <T : KSort> KExpr<T>.castToSort(sort: T): KExpr<T> {
+        if (this.sort == sort || sort !is KArithSort) return this
+
+        val value = uncheckedCast<_, KExpr<KArithSort>>().toRealValue() ?: return this
+
+        return ctx.castRealValue(value, sort).uncheckedCast()
     }
 
     override fun <T : KSort> interpretation(decl: KDecl<T>): KFuncInterp<T>? =

ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/ModelEvalSortTest.kt

@@ -0,0 +1,37 @@
+package io.ksmt.solver.z3
+
+import io.ksmt.KContext
+import io.ksmt.solver.KSolverStatus
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+/**
+ * Z3 assigns the Real sort to `(^ a b)` even when both `a` and `b` are Int sorted,
+ * while in ksmt such an expression is Int sorted.
+ * Because of this, a model value of an Int sorted expression may be a Real numeral.
+ * */
+class ModelEvalSortTest {
+    private val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+    @Test
+    fun testIntPowerModelValueSort() = with(ctx) {
+        KZ3Solver(this).use { solver ->
+            val base = mkConst("base", intSort)
+            val power = mkConst("power", intSort)
+            val expr = mkArithPowerNoSimplify(base, power)
+
+            solver.assert(base eq 2.expr)
+            solver.assert(power eq 2.expr)
+
+            assertEquals(KSolverStatus.SAT, solver.check())
+
+            val model = solver.model()
+            val value = model.eval(expr)
+            val detachedValue = model.detach().eval(expr)
+
+            assertEquals(intSort, value.sort)
+            assertEquals(4.expr, value)
+            assertEquals(detachedValue, value)
+        }
+    }
+}

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

@@ -21,7 +21,7 @@ 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 = "5.0.0"
 
 val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll")
 val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so")
@@ -30,9 +30,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-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),
+    Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-13.3", macDylibPath), null),
+    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.3", macDylibPath), null),
+    Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.38", linuxSoPath), null),
 )
 
 z3Binaries.forEach { it.first.compileClasspath = compileConfig }