Merge pull request #3057 from apalache-mc/th/upgrade-z3

Upgrade Z3 (restores linux/arm64 support)
apalache-mc · Jan 4, 2025 · 512fc1c · 512fc1c
2 parents adc2403 + 4d89d2b
commit 512fc1c
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/.unreleased/breaking-changes/3057-z3.md b/.unreleased/breaking-changes/3057-z3.md
@@ -0,0 +1 @@
+Upgrade Z3 to 4.13.4 (restores linux/arm64 support), see #3057
diff --git 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"

diff --git 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
 ```

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
@@ -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) =>
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Upgrade Z3 to 4.13.4 (restores linux/arm64 support), see #3057