Merge branch 'main' into update/z3-turnkey-4.13.4

.unreleased/breaking-changes/3057-z3.md

@@ -0,0 +1 @@
+Upgrade Z3 to 4.13.4 (restores linux/arm64 support), see #3057

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

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