From 769d7dabd809a41e73bdac4ee4803357c12ebae7 Mon Sep 17 00:00:00 2001 From: Niyaz Nigmatullin Date: Tue, 1 Aug 2023 13:10:06 +0300 Subject: [PATCH] Try to support z3 on arm64 linux --- ksmt-z3/build.gradle.kts | 8 +++++--- .../src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt | 1 + 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/ksmt-z3/build.gradle.kts b/ksmt-z3/build.gradle.kts index d02076cad..e4dc6853e 100644 --- a/ksmt-z3/build.gradle.kts +++ b/ksmt-z3/build.gradle.kts @@ -9,7 +9,7 @@ repositories { mavenCentral() } -val z3Version = "4.11.2" +val z3Version = "4.12.3" val z3JavaJar by lazy { mkZ3ReleaseDownloadTask("x64-win", "*.jar") } @@ -17,7 +17,8 @@ val z3BinariesWithArch = listOf( "x64" to mkZ3ReleaseDownloadTask("x64-win", "*.dll"), "x64" to mkZ3ReleaseDownloadTask("x64-glibc-2.31", "*.so"), "x64" to mkZ3ReleaseDownloadTask("x64-osx-10.16", "*.dylib"), - "arm" to mkZ3ReleaseDownloadTask("arm64-osx-11.0", "*.dylib") + "arm" to mkZ3ReleaseDownloadTask("arm64-osx-11.0", "*.dylib"), + "arm" to mkZ3ReleaseDownloadTask("arm64-glibc-2.35", "*.so"), ) dependencies { @@ -41,7 +42,8 @@ tasks.withType { fun Project.mkZ3ReleaseDownloadTask(arch: String, artifactPattern: String): TaskProvider { val z3ReleaseBaseUrl = "https://github.com/Z3Prover/z3/releases/download" - val releaseName = "z3-${z3Version}" +// val releaseName = "z3-${z3Version}" + val releaseName = "Nightly" val packageName = "z3-${z3Version}-${arch}.zip" val packageDownloadTarget = buildDir.resolve("dist").resolve(releaseName).resolve(packageName) val downloadUrl = listOf(z3ReleaseBaseUrl, releaseName, packageName).joinToString("/") diff --git a/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt index 3c8c5133d..3f078759e 100644 --- a/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt +++ b/ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt @@ -131,6 +131,7 @@ open class KZ3ExprConverter( Z3_sort_kind.Z3_CHAR_SORT, Z3_sort_kind.Z3_UNKNOWN_SORT -> TODO("$sort is not supported yet") null -> error("z3 sort kind cannot be null") + Z3_sort_kind.Z3_TYPE_VAR -> TODO() } }