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
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"
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
 ```
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) =>