diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml index 4c62baec8..9a35efcf4 100644 --- a/.github/workflows/run-long-tests.yml +++ b/.github/workflows/run-long-tests.yml @@ -100,8 +100,18 @@ jobs: --no-daemon '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}' + show_info: + needs: [setup] + runs-on: ubuntu-latest + steps: + - name: Show test info + run: echo "${{ fromJSON(needs.setup.outputs.matrix-tests) }}" + + - name: Show chunk info + run: echo "${{ fromJSON(needs.setup.outputs.matrix-chunks) }}" + run_tests: - needs: [setup, prepare_test_data] + needs: [setup, show_info, prepare_test_data] continue-on-error: true strategy: matrix: diff --git a/README.md b/README.md index acb84b1f2..def034d79 100644 --- a/README.md +++ b/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.30) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.1) [![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.30") +implementation("io.ksmt:ksmt-core:0.6.1") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.30") +implementation("io.ksmt:ksmt-z3:0.6.1") ``` Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index e01795c9a..bde92ba04 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts @@ -11,7 +11,7 @@ plugins { } group = "io.ksmt" -version = "0.5.30" +version = "0.6.1" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index d14878463..1fb83866e 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -34,7 +34,7 @@ repositories { ```kotlin dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.30") + implementation("io.ksmt:ksmt-core:0.6.1") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.30") + implementation("io.ksmt:ksmt-z3:0.6.1") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.30") + implementation("io.ksmt:ksmt-bitwuzla:0.6.1") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index 273cc78e3..12fed7b59 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.30") + implementation("io.ksmt:ksmt-core:0.6.1") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.30") + implementation("io.ksmt:ksmt-z3:0.6.1") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.30") + implementation("io.ksmt:ksmt-runner:0.6.1") } java { diff --git a/ksmt-cvc5/dist/cvc5-1.2.0.jar b/ksmt-cvc5/dist/cvc5-1.2.0.jar deleted file mode 100644 index f68c12e55..000000000 Binary files a/ksmt-cvc5/dist/cvc5-1.2.0.jar and /dev/null differ diff --git a/ksmt-cvc5/dist/cvc5-1.3.0.jar b/ksmt-cvc5/dist/cvc5-1.3.0.jar new file mode 100644 index 000000000..6c33e7f6c Binary files /dev/null and b/ksmt-cvc5/dist/cvc5-1.3.0.jar differ diff --git a/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.2.0.zip b/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip similarity index 54% rename from ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.2.0.zip rename to ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip index 1906edbcc..5d4fe0a45 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.2.0.zip and b/ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.3.0.zip differ diff --git a/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.2.0.zip b/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip similarity index 51% rename from ksmt-cvc5/dist/cvc5-native-osx-arm64-1.2.0.zip rename to ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip index 59e82bcb6..72a884aa6 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.2.0.zip and b/ksmt-cvc5/dist/cvc5-native-osx-arm64-1.3.0.zip differ diff --git a/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.2.0.zip b/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip similarity index 58% rename from ksmt-cvc5/dist/cvc5-native-win-x86-64-1.2.0.zip rename to ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip index e435d55de..c5264f908 100644 Binary files a/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.2.0.zip and b/ksmt-cvc5/dist/cvc5-native-win-x86-64-1.3.0.zip differ diff --git a/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts b/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts index b3f945db2..dd7f549a9 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts +++ b/ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts @@ -11,7 +11,7 @@ repositories { mavenCentral() } -val cvc5Version = "1.2.0" +val cvc5Version = "1.3.0" val cvc5Jar = distDir.resolve("cvc5-$cvc5Version.jar") dependencies { diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt index 87b7570b7..1f34145a1 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt @@ -255,6 +255,15 @@ open class KCvc5ExprConverter( Kind.BITVECTOR_TO_NAT -> expr.convert { bvExpr: KExpr -> mkBv2IntExpr(bvExpr, false) } + + Kind.BITVECTOR_SBV_TO_INT -> expr.convert { bvExpr: KExpr -> + mkBv2IntExpr(bvExpr, isSigned = true) + } + + Kind.BITVECTOR_UBV_TO_INT -> expr.convert { bvExpr: KExpr -> + mkBv2IntExpr(bvExpr, isSigned = false) + } + Kind.BITVECTOR_COMP -> throw KSolverUnsupportedFeatureException( "No direct mapping of ${Kind.BITVECTOR_COMP} in ksmt" ) @@ -430,6 +439,8 @@ open class KCvc5ExprConverter( Kind.SET_MAP, Kind.SET_FILTER, Kind.SET_IS_EMPTY, + Kind.SET_ALL, + Kind.SET_SOME, Kind.SET_FOLD -> throw KSolverUnsupportedFeatureException("currently ksmt does not support sets") Kind.RELATION_JOIN, @@ -460,6 +471,8 @@ open class KCvc5ExprConverter( Kind.BAG_FILTER, Kind.BAG_FOLD, Kind.BAG_SETOF, + Kind.BAG_ALL, + Kind.BAG_SOME, Kind.BAG_PARTITION -> throw KSolverUnsupportedFeatureException("currently ksmt does not support bags") Kind.TABLE_PRODUCT, diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt index 39dae685d..7deb73ae1 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt @@ -158,11 +158,11 @@ import io.ksmt.expr.KXorExpr import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoOverflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvDivNoOverflowExpr +import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr +import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoOverflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvSubNoUnderflowExpr -import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoOverflowExpr -import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.simplifyBvRotateLeftExpr import io.ksmt.expr.rewrite.simplify.simplifyBvRotateRightExpr import io.ksmt.solver.KSolverUnsupportedFeatureException @@ -183,8 +183,6 @@ import io.ksmt.sort.KFpSort import io.ksmt.sort.KRealSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort -import io.ksmt.utils.powerOfTwo -import java.math.BigInteger @Suppress("LargeClass") class KCvc5ExprInternalizer( @@ -580,26 +578,13 @@ class KCvc5ExprInternalizer( } } - // custom implementation - @Suppress("MagicNumber") override fun transform(expr: KBv2IntExpr) = with(expr) { transform(value) { value: Term -> - // by default, it is unsigned in cvc5 - val intTerm = tm.mkTerm(Kind.BITVECTOR_TO_NAT, value) - - if (isSigned) { - val size = this.value.sort.sizeBits.toInt() - val modulo = powerOfTwo(size.toUInt()) - val maxInt = (powerOfTwo((size - 1).toUInt())) - BigInteger.ONE - - val moduloTerm = tm.builder { mkInteger(modulo.toString(10)) } - val maxIntTerm = tm.builder { mkInteger(maxInt.toString(10)) } - - val gtTerm = tm.mkTerm(Kind.GT, intTerm, maxIntTerm) - val subTerm = tm.mkTerm(Kind.SUB, intTerm, moduloTerm) - - tm.mkTerm(Kind.ITE, gtTerm, subTerm, intTerm) - } else intTerm + if (expr.isSigned) { + tm.mkTerm(Kind.BITVECTOR_SBV_TO_INT, value) + } else { + tm.mkTerm(Kind.BITVECTOR_UBV_TO_INT, value) + } } } diff --git a/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts b/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts index d2db8dba0..2ff1fb872 100644 --- a/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts +++ b/ksmt-cvc5/ksmt-cvc5-native/build.gradle.kts @@ -29,7 +29,7 @@ val cvc5Binaries = mapOf( cvc5Binaries.keys.forEach { it.compileClasspath = compileConfig } -val cvc5Version = "1.2.0" +val cvc5Version = "1.3.0" dependencies { compileConfig(project(":ksmt-cvc5:ksmt-cvc5-core")) diff --git a/ksmt-yices/dist/com.sri.yices.jar b/ksmt-yices/dist/com.sri.yices.jar index 5760c3d38..821c55685 100644 Binary files a/ksmt-yices/dist/com.sri.yices.jar and b/ksmt-yices/dist/com.sri.yices.jar differ diff --git a/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip b/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip index d3e9acf3e..54045a6fc 100644 Binary files a/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip and b/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip differ diff --git a/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip b/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip index cee2a43db..f88ac6859 100644 Binary files a/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip and b/ksmt-yices/dist/yices-native-osx-arm64-0.0.zip differ diff --git a/ksmt-yices/dist/yices-native-win32-x86-64-0.0.zip b/ksmt-yices/dist/yices-native-win32-x86-64-0.0.zip index 9144e8377..19aec3fc3 100644 Binary files a/ksmt-yices/dist/yices-native-win32-x86-64-0.0.zip and b/ksmt-yices/dist/yices-native-win32-x86-64-0.0.zip differ diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt index 9e968796b..56ae146bb 100644 --- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt +++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt @@ -9,25 +9,18 @@ import io.ksmt.decl.KDecl import io.ksmt.decl.KFuncDecl import io.ksmt.expr.KExpr import io.ksmt.expr.KUninterpretedSortValue +import io.ksmt.solver.KModel import io.ksmt.solver.model.KFuncInterp import io.ksmt.solver.model.KFuncInterpEntryVarsFree import io.ksmt.solver.model.KFuncInterpVarsFree -import io.ksmt.solver.KModel import io.ksmt.solver.model.KModelEvaluator import io.ksmt.solver.model.KModelImpl -import io.ksmt.sort.KArray2Sort -import io.ksmt.sort.KArray3Sort -import io.ksmt.sort.KArrayNSort -import io.ksmt.sort.KArraySort import io.ksmt.sort.KArraySortBase import io.ksmt.sort.KBoolSort import io.ksmt.sort.KBvSort -import io.ksmt.sort.KFpRoundingModeSort -import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort import io.ksmt.sort.KSort -import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort import io.ksmt.utils.uncheckedCast @@ -46,35 +39,44 @@ class KYicesModel( model.collectDefinedTerms().mapTo(hashSetOf()) { converter.convertDecl(it) } } - override val uninterpretedSorts: Set by lazy { - uninterpretedSortDependencies.keys - } + private val uninterpretedSortValueIndex by lazy { hashMapOf, Int>() } - private val uninterpretedSortDependencies: Map>> by lazy { - val sortsWithDependencies = hashMapOf>>() - val sortCollector = UninterpretedSortCollector(sortsWithDependencies) - declarations.forEach { sortCollector.collect(it) } - sortsWithDependencies - } + private fun uninterpretedSortValueIdx(valueId: Int, sortId: Int): Int = + uninterpretedSortValueIndex.getOrPut(valueId to sortId) { + yicesCtx.convertUninterpretedSortValueIndex(valueId) + } - private val uninterpretedSortUniverse = - hashMapOf>() + private val uninterpretedSortUniverse: Map> by lazy { + val values = model.uninterpretedSortValues() - private val knownUninterpretedSortValues = - hashMapOf>() + val sortValues = hashMapOf>() + for (value in values) { + val (valueId, internalizedSort) = model.scalarValue(value) + val valueIdx = uninterpretedSortValueIdx(valueId, internalizedSort) + sortValues.getOrPut(internalizedSort, ::hashSetOf).add(valueIdx) + } - private val interpretations = hashMapOf, KFuncInterp<*>>() - private val funcInterpretationsToDo = arrayListOf>>() + val result = hashMapOf>() + for ((internalizedSort, valueIndices) in sortValues) { + val sort = converter.convertSort(internalizedSort) + check(sort is KUninterpretedSort) { "Unexpected sort with uninterpreted value: $sort" } + val sortUniverse = valueIndices.mapTo(hashSetOf()) { + ctx.mkUninterpretedSortValue(sort, it) + } + result[sort] = sortUniverse + } - override fun uninterpretedSortUniverse( - sort: KUninterpretedSort - ): Set? = uninterpretedSortUniverse.getOrPut(sort) { - val sortDependencies = uninterpretedSortDependencies[sort] ?: return null + result + } - sortDependencies.forEach { interpretation(it) } + override val uninterpretedSorts: Set + get() = uninterpretedSortUniverse.keys - knownUninterpretedSortValues[sort]?.values?.toHashSet() ?: hashSetOf() - } + private val interpretations = hashMapOf, KFuncInterp<*>>() + private val funcInterpretationsToDo = arrayListOf>>() + + override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? = + uninterpretedSortUniverse[sort] private val evaluatorWithModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = true) } private val evaluatorWithoutModelCompletion by lazy { KModelEvaluator(ctx, this, isComplete = false) } @@ -93,12 +95,9 @@ class KYicesModel( is KRealSort -> mkRealNum(model.bigRationalValue(yval)) is KIntSort -> mkIntNum(model.bigRationalValue(yval)) is KUninterpretedSort -> { - val uninterpretedSortValueId = model.scalarValue(yval)[0] - val sortValues = knownUninterpretedSortValues.getOrPut(sort) { hashMapOf() } - sortValues.getOrPut(uninterpretedSortValueId) { - val valueIndex = yicesCtx.convertUninterpretedSortValueIndex(uninterpretedSortValueId) - mkUninterpretedSortValue(sort, valueIndex) - } + val (uninterpretedSortValueId, sortTypeId) = model.scalarValue(yval) + val valueIndex = uninterpretedSortValueIdx(uninterpretedSortValueId, sortTypeId) + mkUninterpretedSortValue(sort, valueIndex) } is KArraySortBase<*> -> { val funcDecl = ctx.mkFreshFuncDecl("array", sort.range, sort.domainSorts) @@ -184,52 +183,4 @@ class KYicesModel( nativeModel?.close() nativeModel = null } - - private class UninterpretedSortCollector( - private val sorts: MutableMap>> - ) : KSortVisitor { - private lateinit var currentDecl: KDecl<*> - - fun collect(decl: KDecl<*>) { - currentDecl = decl - - decl.sort.accept(this) - decl.argSorts.forEach { it.accept(this) } - } - - override fun visit(sort: KArraySort) { - sort.range.accept(this) - sort.domain.accept(this) - } - - override fun visit(sort: KArray2Sort) { - sort.range.accept(this) - sort.domain0.accept(this) - sort.domain1.accept(this) - } - - override fun visit(sort: KArray3Sort) { - sort.range.accept(this) - sort.domain0.accept(this) - sort.domain1.accept(this) - sort.domain2.accept(this) - } - - override fun visit(sort: KArrayNSort) { - sort.range.accept(this) - sort.domainSorts.forEach { it.accept(this) } - } - - override fun visit(sort: KUninterpretedSort) { - val sortDependencies = sorts.getOrPut(sort) { hashSetOf() } - sortDependencies.add(currentDecl) - } - - override fun visit(sort: KBoolSort) = Unit - override fun visit(sort: KIntSort) = Unit - override fun visit(sort: KRealSort) = Unit - override fun visit(sort: S) = Unit - override fun visit(sort: S) = Unit - override fun visit(sort: KFpRoundingModeSort) = Unit - } } diff --git a/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/SolverTest.kt b/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/SolverTest.kt index b62d6039e..e3ec896d6 100644 --- a/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/SolverTest.kt +++ b/ksmt-yices/ksmt-yices-core/src/test/kotlin/io/ksmt/solver/yices/SolverTest.kt @@ -137,4 +137,49 @@ class SolverTest { assertEquals(KSolverStatus.UNKNOWN, status) } + @Test + fun testUninterpretedSortValueModel(): Unit = with(ctx) { + KYicesSolver(this).use { solver -> + val sort = mkUninterpretedSort("sort") + + val value = mkUninterpretedSortValue(sort, 0) + val a by sort + + solver.assert(a neq value) + solver.check() + + val model = solver.model() + val sortValues = model.uninterpretedSortUniverse(sort)!! + + assertTrue { value in sortValues } + assertTrue { sortValues.size >= 2 } + } + } + + @Test + fun testUninterpretedSortMultipleValueModel(): Unit = with(ctx) { + KYicesSolver(this).use { solver -> + val s1 = mkUninterpretedSort("s1") + val s2 = mkUninterpretedSort("s2") + + val s1value = mkUninterpretedSortValue(s1, 1) + val s2value = mkUninterpretedSortValue(s2, 1) + val s1Var by s1 + val s2Var by s2 + + solver.assert(s1Var neq s1value) + solver.assert(s2Var neq s2value) + solver.check() + + val model = solver.model() + val s1Values = model.uninterpretedSortUniverse(s1)!! + val s2Values = model.uninterpretedSortUniverse(s2)!! + + assertTrue { s1value in s1Values } + assertTrue { s1Values.size >= 2 } + + assertTrue { s2value in s2Values } + assertTrue { s2Values.size >= 2 } + } + } } diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.13.4.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip similarity index 99% rename from ksmt-z3/dist/z3-native-linux-x86-64-4.13.4.zip rename to ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip index 4ad41dc96..053de40c5 100644 Binary files a/ksmt-z3/dist/z3-native-linux-x86-64-4.13.4.zip and b/ksmt-z3/dist/z3-native-linux-x86-64-4.15.3.zip differ diff --git a/ksmt-z3/ksmt-z3-core/build.gradle.kts b/ksmt-z3/ksmt-z3-core/build.gradle.kts index 0ddb45828..31b313d6b 100644 --- a/ksmt-z3/ksmt-z3-core/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-core/build.gradle.kts @@ -9,7 +9,7 @@ repositories { mavenCentral() } -val z3Version = "4.13.4" +val z3Version = "4.15.3" val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", listOf("**/com.microsoft.z3.jar")) } diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index b7cf5f4f1..89306c80d 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/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.13.4" +val z3Version = "4.15.3" val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll") val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so") @@ -30,8 +30,8 @@ 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.1", macDylibPath), null), - Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-13.7.1", macDylibPath), null), + 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), )