From d4268eae94ddb579c5ab144cfe7007cde9ba7e4c Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 3 Jan 2025 13:54:11 +0000 Subject: [PATCH 1/4] Update Z3 --- project/Dependencies.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project/Dependencies.scala b/project/Dependencies.scala index af0ee798cd..84e65197fa 100644 --- a/project/Dependencies.scala +++ b/project/Dependencies.scala @@ -36,7 +36,7 @@ object Dependencies { val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT" val ujson = "com.lihaoyi" %% "ujson" % "4.0.2" val upickle = "com.lihaoyi" %% "upickle" % "4.0.2" - val z3 = "tools.aqua" % "z3-turnkey" % "4.12.6" + val z3 = "tools.aqua" % "z3-turnkey" % "4.13.4" val zio = "dev.zio" %% "zio" % zioVersion // Keep up to sync with version in plugins.sbt val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided" From cae2215247f3fca3ed4fdec9ee2c973b19a702ee Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 3 Jan 2025 13:58:09 +0000 Subject: [PATCH 2/4] Remove Z3 param "seed" It looks like the legacy parameter `seed` has been removed. If we try to pass it, `Solver.add` fails with ``` com.microsoft.z3.Z3Exception: unknown parameter 'seed' Legal parameters are: ... ``` Only `random_seed` remains in the list. --- .../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 2b94cb6317..2f34f0c62c 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -61,8 +61,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL val params = z3context.mkParams() // Set random seed. We are also setting it via global parameters above, but `Global.setParameter()` says: // "When a Z3 module is initialized it will use the value of these parameters when Z3_params objects are not provided." - params.add("seed", config.randomSeed) - // When the user sets z3.smt.logic = QF_LIA, z3 complains about random_seed. + // Note: when the user sets z3.smt.logic = QF_LIA, z3 complains about random_seed. // https://github.com/apalache-mc/apalache/issues/2989 params.add("random_seed", config.randomSeed) config.z3Params.foreach { case (k, v) => From cdaa756c6d27c80546cb531af6fce0275ec82680 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 3 Jan 2025 14:05:28 +0000 Subject: [PATCH 3/4] Add changelog --- .unreleased/breaking-changes/3057-z3.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/breaking-changes/3057-z3.md diff --git a/.unreleased/breaking-changes/3057-z3.md b/.unreleased/breaking-changes/3057-z3.md new file mode 100644 index 0000000000..342ccf1029 --- /dev/null +++ b/.unreleased/breaking-changes/3057-z3.md @@ -0,0 +1 @@ +Upgrade Z3 to 4.13.4 (restores linux/arm64 support), see #3057 From 4d89d2bace3a9fdcfdb41555aadcaa9cdb58ca15 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 3 Jan 2025 16:28:36 +0100 Subject: [PATCH 4/4] Remove Z3 seed parameter from SMT log --- test/tla/cli-integration-tests.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 676077e0d7..26c961c9a7 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -2065,7 +2065,7 @@ $ find ./test-out-dir/Counter.tla/* -type f -name log0.smt -exec cat {} \; ;; sat.random_seed = 0 ;; sls.random_seed = 0 ;; smt.random_seed = 0 -;; (params seed 0 random_seed 0) +;; (params random_seed 0) ... $ rm -rf ./test-out-dir ``` @@ -2082,7 +2082,7 @@ $ find ./test-out-dir/Counter.tla/* -type f -name log0.smt -exec cat {} \; ;; sat.random_seed = 4242 ;; sls.random_seed = 4242 ;; smt.random_seed = 4242 -;; (params seed 4242 random_seed 4242) +;; (params random_seed 4242) ... $ rm -rf ./test-out-dir ```