From edf34283f6d6e5664e322c3948b1eab667eeabd5 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Wed, 20 Mar 2024 16:30:44 +0000
Subject: [PATCH 01/27] Update sbt-buildinfo to 0.12.0

---
 project/plugins.sbt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/plugins.sbt b/project/plugins.sbt
index b82576ce65..737c0b510c 100644
--- a/project/plugins.sbt
+++ b/project/plugins.sbt
@@ -7,7 +7,7 @@ addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0")
 // https://github.com/scoverage/sbt-scoverage
 addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.0.11")
 // https://github.com/sbt/sbt-buildinfo
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.11.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.12.0")
 // https://github.com/sbt/sbt-native-packager
 addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.9.16")
 // https://scalacenter.github.io/scalafix/docs/users/installation.html

From 8a27327d15f0ebbbc410377d72a85dd6a000579e Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Tue, 9 Apr 2024 15:33:27 +0000
Subject: [PATCH 02/27] Update commons-io to 2.16.1

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..6aa0200da7 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -21,7 +21,7 @@ object Dependencies {
     val commonsBeanutils =
       "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2
     val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.9.0"
-    val commonsIo = "commons-io" % "commons-io" % "2.15.1"
+    val commonsIo = "commons-io" % "commons-io" % "2.16.1"
     val guice = "com.google.inject" % "guice" % "7.0.0"
     val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1"
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion

From 4d358538349e806cb466d775843dad63ea65e3b7 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 15 Apr 2024 15:55:32 +0000
Subject: [PATCH 03/27] Update z3-turnkey to 4.12.6

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..fed208cbe0 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" % "3.2.0"
     val upickle = "com.lihaoyi" %% "upickle" % "3.2.0"
-    val z3 = "tools.aqua" % "z3-turnkey" % "4.12.5"
+    val z3 = "tools.aqua" % "z3-turnkey" % "4.12.6"
     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 607d38bd36b78a5b73158b8b7f20c40673629ce3 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Fri, 19 Apr 2024 16:19:34 +0000
Subject: [PATCH 04/27] Update logback-classic, logback-core to 1.5.6

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..32367b9fbf 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -12,7 +12,7 @@ object Dependencies {
 
   object Deps {
     // Versions
-    lazy val logbackVersion = "1.5.3"
+    lazy val logbackVersion = "1.5.6"
     lazy val clistVersion = "3.5.1"
 
     // Libraries

From f6a04b8e266031019c64357ac695d9bd0087a796 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 26 Jun 2024 10:49:24 +0200
Subject: [PATCH 05/27] Translate Quint generate to Apalache!Gen

---
 .../at/forsyte/apalache/io/quint/Quint.scala  | 21 +++++++++++++++++++
 .../apalache/io/quint/TestQuintEx.scala       | 11 ++++++++--
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
index fc16c54ec2..580ae8304b 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -666,6 +666,17 @@ class Quint(quintOutput: QuintOutput) {
         tlaDomain <- tlaExpression(domain)
         tlaScope <- tlaExpression(scope)
       } yield tla.exists(tlaName, tlaDomain, tlaScope)
+
+    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound))), scope) =>
+      val elemType = typeConv.convert(types(id).typ)
+      val boundIntConst = intFromExpr(bound)
+      if (boundIntConst.isEmpty) {
+        throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant")
+      }
+      for {
+        tlaScope <- tlaExpression(scope)
+      } yield tla.letIn(tlaScope, tla.decl(name, tla.gen(boundIntConst.get, elemType)))
+
     case invalidValue =>
       throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}")
   }
@@ -804,4 +815,14 @@ class Quint(quintOutput: QuintOutput) {
         .reverse // Return the declarations to their original order
     }
   } yield TlaModule(module.name, declarations)
+
+  private def intFromExpr(expr: QuintEx): Option[BigInt] = {
+    expr match {
+      case QuintInt(_, value) =>
+        Some(value)
+
+      case _ =>
+        None
+    }
+  }
 }
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
index 06dfd20177..2926d73dee 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -172,7 +172,10 @@ class TestQuintEx extends AnyFunSuite {
     val chooseSomeFromIntSet = app("chooseSome", intSet)(QuintIntT())
     val oneOfSet = app("oneOf", intSet)(QuintIntT())
     val nondetBinding =
-      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintIntT())
+      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
+    val generateSet = app("generate", _42)(QuintSetT(QuintIntT()))
+    val nondetGenerate =
+      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", generateSet), QuintIntT()), tt), QuintBoolT())
     // Requires ID registered with type
     val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
     val addOne = app("iadd", name, _1)(QuintIntT())
@@ -710,10 +713,14 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(Q.app("put", Q.intMap, Q._3, Q._42)(intMapT)) == expected)
   }
 
-  test("can convert nondet bindings") {
+  test("can convert nondet...oneOf") {
     assert(convert(Q.nondetBinding) == "∃n ∈ {1, 2, 3}: (n > 0)")
   }
 
+  test("can convert nondet...generate") {
+    assert(convert(Q.nondetGenerate) == "LET n ≜ Apalache!Gen(42) IN TRUE")
+  }
+
   test("can convert let binding with reference to name in scope") {
     assert(convert(Q.letNbe42inNisGreaterThan0) == "LET n ≜ 42 IN n() > 0")
   }

From fee926c53bd54514506a8b0b81605f69d233f15c Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 26 Jun 2024 22:20:58 +0200
Subject: [PATCH 06/27] fix the signature

---
 .../src/main/scala/at/forsyte/apalache/io/quint/Quint.scala | 6 +++---
 .../scala/at/forsyte/apalache/io/quint/TestQuintEx.scala    | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
index 580ae8304b..eaa4fb1a8f 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -667,15 +667,15 @@ class Quint(quintOutput: QuintOutput) {
         tlaScope <- tlaExpression(scope)
       } yield tla.exists(tlaName, tlaDomain, tlaScope)
 
-    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound))), scope) =>
-      val elemType = typeConv.convert(types(id).typ)
+    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(_, bound))), scope) =>
+      val setType = typeConv.convert(types(id).typ)
       val boundIntConst = intFromExpr(bound)
       if (boundIntConst.isEmpty) {
         throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant")
       }
       for {
         tlaScope <- tlaExpression(scope)
-      } yield tla.letIn(tlaScope, tla.decl(name, tla.gen(boundIntConst.get, elemType)))
+      } yield tla.letIn(tlaScope, tla.decl(name, tla.gen(boundIntConst.get, setType)))
 
     case invalidValue =>
       throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}")
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
index 2926d73dee..273ee5ad03 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -173,7 +173,7 @@ class TestQuintEx extends AnyFunSuite {
     val oneOfSet = app("oneOf", intSet)(QuintIntT())
     val nondetBinding =
       e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
-    val generateSet = app("generate", _42)(QuintSetT(QuintIntT()))
+    val generateSet = app("generate", _42, _42)(QuintSetT(QuintIntT()))
     val nondetGenerate =
       e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", generateSet), QuintIntT()), tt), QuintBoolT())
     // Requires ID registered with type

From 7351a7e5ce717cb5a5c439e8dde70feca99e77de Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 27 Jun 2024 10:15:47 +0200
Subject: [PATCH 07/27] properly translate Quint's generate

---
 .../scala/at/forsyte/apalache/io/quint/Quint.scala | 14 ++++++++++----
 .../at/forsyte/apalache/io/quint/TestQuintEx.scala | 10 +++++++---
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
index eaa4fb1a8f..5c965f921f 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala
@@ -655,9 +655,13 @@ class Quint(quintOutput: QuintOutput) {
 
   // Convert Quint's nondet variable binding
   //
-  //   val nondet name = oneOf(domain); scope
+  //   nondet name = oneOf(domain); scope
   //   ~~>
   //   \E name \in domain: scope
+  //
+  //   nondet name = generate(sz, typeSet); scope
+  //   ~~>
+  //   \E name \in { Apalache!Gen(sz) }: scope
   private val nondetBinding: (QuintDef.QuintOpDef, QuintEx) => NullaryOpReader[TBuilderInstruction] = {
     case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "oneOf", Seq(domain))), scope) =>
       val elemType = typeConv.convert(types(id).typ)
@@ -667,15 +671,17 @@ class Quint(quintOutput: QuintOutput) {
         tlaScope <- tlaExpression(scope)
       } yield tla.exists(tlaName, tlaDomain, tlaScope)
 
-    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(_, bound))), scope) =>
-      val setType = typeConv.convert(types(id).typ)
+    case (QuintDef.QuintOpDef(_, name, "nondet", QuintApp(id, "generate", Seq(bound, _))), scope) =>
+      val elemType = typeConv.convert(types(id).typ)
       val boundIntConst = intFromExpr(bound)
       if (boundIntConst.isEmpty) {
         throw new QuintIRParseError(s"nondet $name = generate($bound) ... expects an integer constant")
       }
+      val genExpr = tla.enumSet(tla.gen(boundIntConst.get, elemType))
+      val tlaName = tla.name(name, elemType)
       for {
         tlaScope <- tlaExpression(scope)
-      } yield tla.letIn(tlaScope, tla.decl(name, tla.gen(boundIntConst.get, setType)))
+      } yield tla.exists(tlaName, genExpr, tlaScope)
 
     case invalidValue =>
       throw new QuintIRParseError(s"nondet keyword used to bind invalid value ${invalidValue}")
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
index 273ee5ad03..9dc52d9da4 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -173,9 +173,13 @@ class TestQuintEx extends AnyFunSuite {
     val oneOfSet = app("oneOf", intSet)(QuintIntT())
     val nondetBinding =
       e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
-    val generateSet = app("generate", _42, _42)(QuintSetT(QuintIntT()))
+    val generateSet = app("generate", _42, app("Set", _42)(QuintSetT(QuintIntT())))(QuintSetT(QuintIntT()))
+    val nondetGenerateId = uid
+    val appGenSet = app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT())
     val nondetGenerate =
-      e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", generateSet), QuintIntT()), tt), QuintBoolT())
+      e(QuintLet(uid,
+        d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet), QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet),
+        QuintBoolT())
     // Requires ID registered with type
     val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
     val addOne = app("iadd", name, _1)(QuintIntT())
@@ -718,7 +722,7 @@ class TestQuintEx extends AnyFunSuite {
   }
 
   test("can convert nondet...generate") {
-    assert(convert(Q.nondetGenerate) == "LET n ≜ Apalache!Gen(42) IN TRUE")
+    assert(convert(Q.nondetGenerate) == "∃S ∈ {Apalache!Gen(42)}: (S = {})")
   }
 
   test("can convert let binding with reference to name in scope") {

From 74080d84d30f13648408de606bb188b051181df1 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 27 Jun 2024 19:37:36 +0200
Subject: [PATCH 08/27] add release notes

---
 .unreleased/features/translate-generate.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 .unreleased/features/translate-generate.md

diff --git a/.unreleased/features/translate-generate.md b/.unreleased/features/translate-generate.md
new file mode 100644
index 0000000000..326f24450d
--- /dev/null
+++ b/.unreleased/features/translate-generate.md
@@ -0,0 +1 @@
+Translate Quint's generate into `Apalache!Gen` (#2916)

From 5b5f6afa752cd60817811d09746cef45ebc952d7 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 27 Jun 2024 19:44:16 +0200
Subject: [PATCH 09/27] fix formatting

---
 .../scala/at/forsyte/apalache/io/quint/TestQuintEx.scala   | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
index 9dc52d9da4..ee84a40fb5 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala
@@ -175,11 +175,12 @@ class TestQuintEx extends AnyFunSuite {
       e(QuintLet(uid, d(QuintDef.QuintOpDef(uid, "n", "nondet", oneOfSet), QuintIntT()), nIsGreaterThan0), QuintBoolT())
     val generateSet = app("generate", _42, app("Set", _42)(QuintSetT(QuintIntT())))(QuintSetT(QuintIntT()))
     val nondetGenerateId = uid
-    val appGenSet = app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT())
+    val appGenSet =
+      app("eq", e(QuintName(uid, "S"), QuintSetT(QuintIntT())), app("Set")(QuintSetT(QuintIntT())))(QuintBoolT())
     val nondetGenerate =
       e(QuintLet(uid,
-        d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet), QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet),
-        QuintBoolT())
+              d(QuintDef.QuintOpDef(nondetGenerateId, "S", "nondet", generateSet),
+                  QuintOperT(Seq(), QuintSetT(QuintIntT()))), appGenSet), QuintBoolT())
     // Requires ID registered with type
     val selectGreaterThanZero = app("select", intList, intIsGreaterThanZero)(QuintSeqT(QuintIntT()))
     val addOne = app("iadd", name, _1)(QuintIntT())

From a12573fdea7c8b7d42129628ca59686bc0b310fb Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Wed, 10 Jul 2024 16:00:44 +0000
Subject: [PATCH 10/27] Update sbt to 1.10.1

---
 project/build.properties                        | 2 +-
 project/sbt-changeling/build.sbt                | 2 +-
 project/sbt-changeling/project/build.properties | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/project/build.properties b/project/build.properties
index 04267b14af..ee4c672cd0 100644
--- a/project/build.properties
+++ b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.9.9
+sbt.version=1.10.1
diff --git a/project/sbt-changeling/build.sbt b/project/sbt-changeling/build.sbt
index 2d86b9cb52..2df02ef524 100644
--- a/project/sbt-changeling/build.sbt
+++ b/project/sbt-changeling/build.sbt
@@ -2,7 +2,7 @@ ThisBuild / version := "0.1.0-SNAPSHOT"
 ThisBuild / organization := "systems.informal"
 
 libraryDependencies ++= Seq(
-    "org.scala-sbt" % "sbt" % "1.9.9"
+    "org.scala-sbt" % "sbt" % "1.10.1"
 )
 
 lazy val sbt_changeling = (project in file("."))
diff --git a/project/sbt-changeling/project/build.properties b/project/sbt-changeling/project/build.properties
index 04267b14af..ee4c672cd0 100644
--- a/project/sbt-changeling/project/build.properties
+++ b/project/sbt-changeling/project/build.properties
@@ -1 +1 @@
-sbt.version=1.9.9
+sbt.version=1.10.1

From c89de58ed83bb2d3ad85d0d96f4056d585beca45 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 23 Jul 2024 16:56:50 +0200
Subject: [PATCH 11/27] Create FUNDING.md

---
 FUNDING.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 FUNDING.md

diff --git a/FUNDING.md b/FUNDING.md
new file mode 100644
index 0000000000..95e1d0943f
--- /dev/null
+++ b/FUNDING.md
@@ -0,0 +1,20 @@
+## Apalache Funding
+
+We are grateful to the following organizations for financially supporting
+the project Apalache for significant duration of time in the past:
+
+- [Informal Systems][]: 2020-2024
+- [Vienna Business Agency][]: 2021-2023
+- [Interchain Foundation][]: 2019-2023
+- [WWTF][] (Austria): Vienna Science and Technology Fund 2016-2020
+- [Inria Nancy][] and [LORIA][] (France): 2018-2019
+- [TU Wien][] (Austria): 2016-2020
+
+[WWTF]: https://wwtf.at/index.php?lang=EN
+[TU Wien]: https://www.tuwien.at/
+[Inria Nancy]: https://www.inria.fr/en/inria-centre-universite-lorraine
+[LORIA]: https://loria.fr
+[Interchain Foundation]: https://interchain.io/
+[Informal Systems]: https://informal.systems/
+[Vienna Business Agency]: https://viennabusinessagency.at/
+[Igor Konnov]: https://konnov.phd/

From 465b6a96a731a595e18c478c8df22457e6025abf Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 23 Jul 2024 17:40:16 +0200
Subject: [PATCH 12/27] Update FUNDING.md

Co-authored-by: Gabriela Moreira <gabrielamoreiramafra@gmail.com>
---
 FUNDING.md | 1 -
 1 file changed, 1 deletion(-)

diff --git a/FUNDING.md b/FUNDING.md
index 95e1d0943f..7d6cffe670 100644
--- a/FUNDING.md
+++ b/FUNDING.md
@@ -17,4 +17,3 @@ the project Apalache for significant duration of time in the past:
 [Interchain Foundation]: https://interchain.io/
 [Informal Systems]: https://informal.systems/
 [Vienna Business Agency]: https://viennabusinessagency.at/
-[Igor Konnov]: https://konnov.phd/

From d707272ea466852ce81853197aad72bedc81dc7e Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 29 Jul 2024 16:14:34 +0000
Subject: [PATCH 13/27] Update scalafmt-core to 3.8.3

---
 .scalafmt.conf | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.scalafmt.conf b/.scalafmt.conf
index 11af66aa14..2f274e9290 100644
--- a/.scalafmt.conf
+++ b/.scalafmt.conf
@@ -1,4 +1,4 @@
-version = "3.8.0"
+version = "3.8.3"
 
 runner.dialect = scala213
 fileOverride {

From 60dd752b3c25a2b578b9f0a967878904d6941982 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 29 Jul 2024 16:15:48 +0000
Subject: [PATCH 14/27] Reformat with scalafmt 3.8.3

Executed command: scalafmt --non-interactive
---
 .../at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala     | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala
index 2fee63793c..6ebb57ec76 100644
--- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala
+++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestSetBuilder.scala
@@ -292,7 +292,7 @@ class TestSetBuilder extends BuilderTest {
                   builder.name(s"x$i", ti),
                   builder.name(s"S$i", InvalidTypeMethods.notSet),
               )
-            }
+            },
         )
 
     }
@@ -441,7 +441,7 @@ class TestSetBuilder extends BuilderTest {
           ts.zipWithIndex.map { case ((ti, _), i) =>
             builder.name(s"x$i", ti) ->
               builder.name(s"S$i", InvalidTypeMethods.notSet)
-          }
+          },
       )
     }
 

From b03767c8c14d5008db0721279cc338968ea94f3c Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 29 Jul 2024 16:15:48 +0000
Subject: [PATCH 15/27] Add 'Reformat with scalafmt 3.8.3' to
 .git-blame-ignore-revs

---
 .git-blame-ignore-revs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index 05d4c13a59..71e9c75789 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -6,3 +6,6 @@
 
 # Scala Steward: Reformat with scalafmt 3.7.6
 1b2091c13571348b534076f2183ced2cd2ff67a9
+
+# Scala Steward: Reformat with scalafmt 3.8.3
+60dd752b3c25a2b578b9f0a967878904d6941982

From f624624baf1291b59fa6db5f8a929bc7870138a1 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 5 Aug 2024 19:30:55 +0000
Subject: [PATCH 16/27] Update easymock to 5.4.0

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..b1562a259b 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -54,7 +54,7 @@ object Dependencies {
     // Libraries
     val junit = "junit" % "junit" % "4.13.2" % Test
     val scalacheck = "org.scalacheck" %% "scalacheck" % "1.17.0" % Test
-    val easymock = "org.easymock" % "easymock" % "5.2.0" % Test
+    val easymock = "org.easymock" % "easymock" % "5.4.0" % Test
 
     val scalaTestVersion = "3.2.15"
     val scalatest = "org.scalatest" %% "scalatest" % scalaTestVersion % Test

From d1f04b510bc86c3e8b7318a3a41542ce8227db68 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 12 Aug 2024 21:29:54 +0000
Subject: [PATCH 17/27] Update grpc-netty to 1.66.0

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..0bc3782dcb 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -40,7 +40,7 @@ object Dependencies {
     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"
-    val grpcNetty = "io.grpc" % "grpc-netty" % "1.62.2"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.66.0"
     val scalapbRuntimGrpc =
       "com.thesamet.scalapb" %% "scalapb-runtime-grpc" % scalapb.compiler.Version.scalapbVersion
     // Ensures we have access to commonly used protocol buffers (e.g., google.protobuf.Struct)

From 64d8becac7e2a978ceafc615367c4f8c460e25a5 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Mon, 12 Aug 2024 21:30:18 +0000
Subject: [PATCH 18/27] Update slf4j-api to 2.0.16

---
 project/Dependencies.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 5c0269f1ce..c263e2acdd 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -31,7 +31,7 @@ object Dependencies {
     val scalaParserCombinators = "org.scala-lang.modules" %% "scala-parser-combinators" % "2.3.0"
     val scalaCollectionContrib = "org.scala-lang.modules" %% "scala-collection-contrib" % "0.3.0"
     val scalaz = "org.scalaz" %% "scalaz-core" % "7.3.5"
-    val slf4j = "org.slf4j" % "slf4j-api" % "2.0.12"
+    val slf4j = "org.slf4j" % "slf4j-api" % "2.0.16"
     val shapeless = "com.chuusai" %% "shapeless" % "2.3.10"
     val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT"
     val ujson = "com.lihaoyi" %% "ujson" % "3.2.0"

From 2c7a7e6cdd3f8d8f3c79d69245dc2b1ef75e1725 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 13 Aug 2024 16:40:33 +0200
Subject: [PATCH 19/27] disable docker-tests

---
 .github/workflows/main.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 43f314e500..5a95199b64 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -166,6 +166,8 @@ jobs:
           TEST_FILTER: ${{ matrix.smt-encoding == 'arrays' && 'array-encoding' || '' }}
 
   docker-tests:
+    # provisionally disable docker tests until we repair them
+    if: false
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4

From b54d097637c602412b91dbab87aa0b093114fb53 Mon Sep 17 00:00:00 2001
From: Kukovec <jure.kukovec@gmail.com>
Date: Wed, 14 Aug 2024 12:03:10 +0200
Subject: [PATCH 20/27] Introduce the `Repeat` Apalache operator (#2927)

* Added the Repeat operator

* integration tests + rule fix

* Typo caught by @thpani

* fmt fix

* PR comments

* fmt-fix

---------

Co-authored-by: Igor Konnov <igor@konnov.phd>
---
 docs/src/lang/apalache-operators.md           | 37 +++++++++
 src/tla/Apalache.tla                          | 13 +++
 test/tla/Repeat.tla                           | 66 +++++++++++++++
 test/tla/RepeatBad.tla                        | 11 +++
 test/tla/cli-integration-tests.md             | 18 ++++
 .../tla/bmcmt/SymbStateRewriterImpl.scala     |  4 +-
 .../apalache/tla/bmcmt/rules/RepeatRule.scala | 83 +++++++++++++++++++
 .../apalache/tla/bmcmt/util/TlaExUtil.scala   |  5 ++
 .../tla/bmcmt/TestRewriterWithArrays.scala    |  2 +-
 .../tla/bmcmt/TestRewriterWithFunArrays.scala |  2 +-
 .../tla/bmcmt/TestRewriterWithOOPSLA19.scala  |  2 +-
 .../bmcmt/TestSymbStateRewriterRepeat.scala   | 45 ++++++++++
 .../apalache/io/json/BuilderCallByName.scala  | 10 +++
 .../apalache/tla/imp/StandardLibrary.scala    |  1 +
 .../tla/typecheck/etc/ToEtcExpr.scala         |  6 ++
 .../apalache/tla/lir/oper/ApalacheOper.scala  | 13 +++
 .../standard/KeraLanguagePred.scala           |  5 ++
 .../signatures/ApalacheOperSignatures.scala   |  7 ++
 .../typecomp/subbuilder/ApalacheBuilder.scala | 10 +++
 .../unsafe/UnsafeApalacheBuilder.scala        | 13 +++
 20 files changed, 349 insertions(+), 4 deletions(-)
 create mode 100644 test/tla/Repeat.tla
 create mode 100644 test/tla/RepeatBad.tla
 create mode 100644 tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
 create mode 100644 tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala

diff --git a/docs/src/lang/apalache-operators.md b/docs/src/lang/apalache-operators.md
index 7166c4fc8a..41d1a8c81e 100644
--- a/docs/src/lang/apalache-operators.md
+++ b/docs/src/lang/apalache-operators.md
@@ -142,7 +142,44 @@ IN
 The operators `ApaFoldSet` and `ApaFoldSeqLeft` are explained in more detail in a dedicated section [here](../apalache/principles/folds.md).
 
 ----------------------------------------------------------------------------
+<a name="Repeat"></a>
+## Operator iteration
 
+**Notation:** `Repeat(Op, N, x)`
+
+**LaTeX notation:** `Repeat(Op, N, x)`
+
+**Arguments:** Three arguments: An operator `Op`, an iteration counter `N` (a nonnegative constant integer expression), and an
+initial value `x`.
+
+**Apalache type:** `((a, Int), Int, a) => a`, for some type `a`.
+
+**Effect:** For a given constant bound `N`, computes the value
+`F(F(F(F(x,1), 2), ...), N)`. If `N=0` it evaluates to `x`.
+
+```tla
+Repeat(Op, N, x) ==
+    ApaFoldSeqLeft(Op, x, MkSeq(N, LAMBDA i:i))
+```
+
+Apalache implements a more efficient encoding of this operator than the default one.
+
+**Determinism:** Deterministic.
+
+**Errors:**
+If any argument is ill-typed, or `N` is not a nonnegative constant integer expression, Apalache reports an error.
+
+**Example in TLA+:**
+
+```tla
+Op(a) == a + 1
+LET OpModified(a,i) == Op(i)
+IN Repeat(OpModified, 0, 5) = 5     \* TRUE
+
+Op2(a,i) == a + i
+Repeat(Op2, 0, 5) = 15              \* TRUE
+```
+----------------------------------------------------------------------------
 <a name="SetAsFun"></a>
 
 ## Convert a set of pairs to a function
diff --git a/src/tla/Apalache.tla b/src/tla/Apalache.tla
index b8bb5cb1c5..ea5188fb9b 100644
--- a/src/tla/Apalache.tla
+++ b/src/tla/Apalache.tla
@@ -152,4 +152,17 @@ ApaFoldSeqLeft(__Op(_,_), __v, __seq) ==
     THEN __v
     ELSE ApaFoldSeqLeft(__Op, __Op(__v, Head(__seq)), Tail(__seq))
 
+(**
+ * The repetition operator, used to consecutively apply an operator, starting from
+ * an initial value.
+ *
+ * @type: ((a, Int) => a, Int, a) => a;
+ *)
+RECURSIVE Repeat(_,_,_)
+Repeat(__F(_,_), __N, __x) ==
+        \* This is the TLC implementation. Apalache does it differently.
+        IF __N <= 0
+        THEN __x
+        ELSE __F(Repeat(__F, __N - 1, __x), __N)
+
 ===============================================================================
diff --git a/test/tla/Repeat.tla b/test/tla/Repeat.tla
new file mode 100644
index 0000000000..93aa7adda9
--- /dev/null
+++ b/test/tla/Repeat.tla
@@ -0,0 +1,66 @@
+------------------------ MODULE Repeat ------------------------------------
+EXTENDS Apalache, Integers
+
+Inv1 ==
+    LET Op(a, i) == a + 1
+    IN Repeat(Op, 5, 0) = 5
+
+Inv2 ==
+    LET Op(a, i) == a + i
+    IN Repeat(Op, 5, 0) = 15
+
+\* Cyclical Op: \E k: Op^k = Id
+Inv3 ==
+    LET Op(a,i) == (a + i) % 3
+    IN LET
+        v == 1
+        x0 == Repeat(Op, 0, v)
+        x3 == Repeat(Op, 3, v)
+        x6 == Repeat(Op, 6, v)
+    IN
+        /\ v = x0
+        /\ x0 = x3
+        /\ x3 = x6
+
+\* Idempotent Op: Op^2 = Op
+Inv4 ==
+    LET
+        \* @type: (Set(Set(Int)), Int) => Set(Set(Int));
+        Op(a, i) == {UNION a}
+    IN LET
+        v == {{1}, {2}, {3,4}}
+        x1 == Repeat(Op, 1, v)
+        x2 == Repeat(Op, 2, v)
+        x3 == Repeat(Op, 3, v)
+    IN
+        /\ v /= x1
+        /\ x1 = x2
+        /\ x2 = x3
+
+\* Nilpotent Op: \E k: Op^k = 0
+Inv5 ==
+    LET
+        \* @type: (Set(Int), Int) => Set(Int);
+        Op(a, i) == a \ { x \in a: \A y \in a: x <= y }
+    IN LET
+        v == {1,2,3}
+        x1 == Repeat(Op, 2, v)
+        x2 == Repeat(Op, 3, v)
+        x3 == Repeat(Op, 4, v)
+    IN
+        /\ x1 /= x2
+        /\ x2 = x3
+        /\ x3 = {}
+
+
+Init == TRUE
+Next == TRUE
+
+Inv ==
+    /\ Inv1
+    /\ Inv2
+    /\ Inv3
+    /\ Inv4
+    /\ Inv5
+
+===============================================================================
diff --git a/test/tla/RepeatBad.tla b/test/tla/RepeatBad.tla
new file mode 100644
index 0000000000..3951d35d80
--- /dev/null
+++ b/test/tla/RepeatBad.tla
@@ -0,0 +1,11 @@
+------------------------ MODULE RepeatBad ------------------------------------
+EXTENDS Apalache, Integers
+
+Inv ==
+    LET Op(a, i) == a + 1
+    \* The 2nd argument to Repeat must be an integer literal
+    IN \E x \in {5} : Repeat(Op, x, 0) = 5
+
+Init == TRUE
+Next == TRUE
+===============================================================================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 6cec251917..d2debd6027 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -894,6 +894,24 @@ The outcome is: NoError
 EXITCODE: OK
 ```
 
+### check Repeat succeeds
+
+```sh
+$ apalache-mc check --inv=Inv --length=0 Repeat.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+EXITCODE: OK
+```
+
+### check RepeatBad fails
+
+```sh
+$ apalache-mc check --inv=Inv --length=0 RepeatBad.tla | sed 's/I@.*//'
+...
+EXITCODE: ERROR (255)
+```
+
 ### check Counter.tla errors (array-encoding)
 
 ```sh
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
index 11539bc03b..be9b21862c 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
@@ -303,11 +303,13 @@ class SymbStateRewriterImpl(
           -> List(new LabelRule(this)),
         key(OperEx(ApalacheOper.gen, tla.int(2)))
           -> List(new GenRule(this)),
-        // folds and MkSeq
+        // folds, repeat and MkSeq
         key(OperEx(ApalacheOper.foldSet, tla.name("A"), tla.name("v"), tla.name("S")))
           -> List(new FoldSetRule(this, renaming)),
         key(OperEx(ApalacheOper.foldSeq, tla.name("A"), tla.name("v"), tla.name("s")))
           -> List(new FoldSeqRule(this, renaming)),
+        key(OperEx(ApalacheOper.repeat, tla.name("Op"), tla.int(10), tla.name("s")))
+          -> List(new RepeatRule(this, renaming)),
         key(OperEx(ApalacheOper.mkSeq, tla.int(10), tla.name("A")))
           -> List(new MkSeqRule(this, renaming)),
     )
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
new file mode 100644
index 0000000000..7bec841e0a
--- /dev/null
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala
@@ -0,0 +1,83 @@
+package at.forsyte.apalache.tla.bmcmt.rules
+
+import at.forsyte.apalache.tla.bmcmt._
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.lir.oper.ApalacheOper
+import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
+import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming
+import at.forsyte.apalache.tla.lir.values.TlaInt
+import at.forsyte.apalache.tla.pp.Inliner
+import at.forsyte.apalache.tla.types.tla
+
+/**
+ * Rewriting rule for Repeat. This rule is similar to [[FoldSeqRule]].
+ *
+ * This rule is more efficient than the fold- rules, because it does not require an underlying data structure (Seq or
+ * Set). In particular, folding over 1..N, despite the overapproximation being tight by construction, still introduces
+ * O(N*N) constraints, since the SMT solver must assert element uniqueness (i /= j for all i,j \in 1..N). OTOH,
+ * RepeatRule consumes 1..N in the canonical order natively as a 1.to(N) in Scala.
+ *
+ * @author
+ *   Jure Kukovec
+ */
+class RepeatRule(rewriter: SymbStateRewriter, renaming: IncrementalRenaming) extends RewritingRule {
+
+  override def isApplicable(symbState: SymbState): Boolean = {
+    symbState.ex match {
+      case OperEx(ApalacheOper.repeat, LetInEx(NameEx(appName), TlaOperDecl(operName, params, _)), _, _) =>
+        appName == operName && params.size == 2
+      case _ => false
+    }
+  }
+
+  override def apply(state: SymbState): SymbState = state.ex match {
+    // assume isApplicable
+    case ex @ OperEx(ApalacheOper.repeat, LetInEx(NameEx(_), opDecl), boundEx, baseEx) =>
+      boundEx match {
+        case ValEx(TlaInt(n)) if n.isValidInt && n.toInt >= 0 =>
+          // rewrite baseEx to its final cell form
+          val baseState = rewriter.rewriteUntilDone(state.setRex(baseEx))
+
+          // We need the type signature. The signature of Repeat is
+          // \A a : ((a,Int) => a, Int, a) => a
+          // so the operator type must be (a,Int) => a
+          val a = TlaType1.fromTypeTag(baseEx.typeTag)
+          val opT = OperT1(Seq(a, IntT1), a)
+          // sanity check
+          TlaType1.fromTypeTag(opDecl.typeTag) match {
+            case `opT` => // all good
+            case badType =>
+              val msg = s"FoldSet argument ${opDecl.name} should have the tag $opT, found $badType."
+              throw new TypingException(msg, opDecl.ID)
+          }
+
+          // expressions are transient, we don't need tracking
+          val inliner = new Inliner(new IdleTracker, renaming)
+          // We can make the scope directly, since InlinePass already ensures all is well.
+          val seededScope: Inliner.Scope = Map(opDecl.name -> opDecl)
+
+          // To implement the Repeat rule, we generate a sequence of cells.
+          // At each step, we perform one application of the operator
+          // defined by `opDecl` to the previous partial result,
+          // and pass the iteration index as the second parameter
+          (1 to n.toInt).foldLeft(baseState) { case (partialState, i) =>
+            // partialState currently holds the cell representing the previous application step
+            val oldResultCell = partialState.asCell
+
+            // First, we inline the operator application, with cell names as parameters
+            val appEx = tla.appOp(
+                tla.name(opDecl.name, opT),
+                oldResultCell.toBuilder,
+                tla.int(i),
+            )
+
+            val inlinedEx = inliner.transform(seededScope)(appEx)
+            rewriter.rewriteUntilDone(partialState.setRex(inlinedEx))
+          }
+        case _ =>
+          throw new RewriterException("Apalache!Repeat expects a constant positive integer. Found: " + boundEx, ex)
+      }
+    case _ =>
+      throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex)
+  }
+}
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala
index 4010c2c726..68662f3919 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/util/TlaExUtil.scala
@@ -32,6 +32,11 @@ object TlaExUtil {
         findRec(localBody)
         baseExAndCollectionEx.foreach(findRec)
 
+      // ignore the names in the auxiliary let-in definition
+      case OperEx(ApalacheOper.repeat, LetInEx(_, TlaOperDecl(_, _, localBody)), boundAndBaseEx @ _*) =>
+        findRec(localBody)
+        boundAndBaseEx.foreach(findRec)
+
       // ignore the names in the auxiliary let-in definition
       case OperEx(ApalacheOper.mkSeq, len, LetInEx(_, TlaOperDecl(_, _, localBody))) =>
         findRec(localBody)
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala
index 1a79c4efd5..f146e7cbb6 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala
@@ -18,7 +18,7 @@ class TestRewriterWithArrays
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecord with TestSymbStateRewriterSequence
     with TestSymbStateRewriterSet with TestSymbStateRewriterStr with TestSymbStateRewriterTuple
     with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle
-    with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq {
+    with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq with TestSymbStateRewriterRepeat {
   override protected def withFixture(test: OneArgTest): Outcome = {
     solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true,
                 smtEncoding = SMTEncoding.Arrays)))
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala
index a7647d39c6..43b6cc0a18 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithFunArrays.scala
@@ -18,7 +18,7 @@ class TestRewriterWithFunArrays
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecord with TestSymbStateRewriterSequence
     with TestSymbStateRewriterSet with TestSymbStateRewriterStr with TestSymbStateRewriterTuple
     with TestPropositionalOracle with TestSparseOracle with TestUninterpretedConstOracle
-    with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq {
+    with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq with TestSymbStateRewriterRepeat {
   override protected def withFixture(test: OneArgTest): Outcome = {
     solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true,
                 smtEncoding = SMTEncoding.FunArrays)))
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala
index 468aabb431..b455b76665 100644
--- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala
@@ -19,7 +19,7 @@ class TestRewriterWithOOPSLA19
     with TestSymbStateRewriterVariant with TestSymbStateRewriterSequence with TestSymbStateRewriterSet
     with TestSymbStateRewriterStr with TestSymbStateRewriterTuple with TestPropositionalOracle with TestSparseOracle
     with TestUninterpretedConstOracle with TestSymbStateRewriterApalache with TestSymbStateRewriterMkSeq
-    with TestDefaultValueFactory {
+    with TestDefaultValueFactory with TestSymbStateRewriterRepeat {
   override protected def withFixture(test: OneArgTest): Outcome = {
     solverContext = new PreproSolverContext(new Z3SolverContext(SolverConfig.default.copy(debug = true,
                 smtEncoding = SMTEncoding.OOPSLA19)))
diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala
new file mode 100644
index 0000000000..aea018c7dd
--- /dev/null
+++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala
@@ -0,0 +1,45 @@
+package at.forsyte.apalache.tla.bmcmt
+
+import at.forsyte.apalache.infra.passes.options.SMTEncoding
+import at.forsyte.apalache.tla.lir._
+import at.forsyte.apalache.tla.types.tla
+
+trait TestSymbStateRewriterRepeat extends RewriterBase {
+  test("""Repeat(LET Op(a,i) == a + 1 IN Op, 5, 0) = 5""") { rewriterType: SMTEncoding =>
+    // Op(x, i) == x + 1
+    val opT = OperT1(Seq(IntT1, IntT1), IntT1)
+
+    val plusOneEx = tla.plus(tla.name("x", IntT1), tla.int(1))
+    val plusOneOper = tla.decl("Op", plusOneEx, tla.param("x", IntT1), tla.param("i", IntT1))
+    val letEx = tla.letIn(tla.name(plusOneOper.name, opT), plusOneOper)
+    val repeatEx = tla.repeat(letEx, 5, tla.int(0))
+
+    val rewriter = create(rewriterType)
+    var state = new SymbState(repeatEx, arena, Binding())
+    state = rewriter.rewriteUntilDone(state)
+    val asCell = state.asCell
+
+    // compare the value
+    val eqn = tla.eql(asCell.toBuilder, tla.int(5))
+    assertTlaExAndRestore(rewriter, state.setRex(eqn))
+  }
+
+  test("""Repeat(LET Op(a,i) == a + i IN Op, 5, 0) = 15""") { rewriterType: SMTEncoding =>
+    // Op(x, i) == x + i
+    val opT = OperT1(Seq(IntT1, IntT1), IntT1)
+
+    val plusiEx = tla.plus(tla.name("x", IntT1), tla.name("i", IntT1))
+    val plusiOper = tla.decl("Op", plusiEx, tla.param("x", IntT1), tla.param("i", IntT1))
+    val letEx = tla.letIn(tla.name(plusiOper.name, opT), plusiOper)
+    val repeatEx = tla.repeat(letEx, 5, tla.int(0))
+
+    val rewriter = create(rewriterType)
+    var state = new SymbState(repeatEx, arena, Binding())
+    state = rewriter.rewriteUntilDone(state)
+    val asCell = state.asCell
+
+    // compare the value
+    val eqn = tla.eql(asCell.toBuilder, tla.int(15))
+    assertTlaExAndRestore(rewriter, state.setRex(eqn))
+  }
+}
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala
index 94a2443f74..600d10911c 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/json/BuilderCallByName.scala
@@ -103,6 +103,7 @@ object BuilderCallByName {
       ApalacheOper.mkSeq.name -> ApalacheOper.mkSeq,
       ApalacheOper.foldSet.name -> ApalacheOper.foldSet,
       ApalacheOper.foldSeq.name -> ApalacheOper.foldSeq,
+      ApalacheOper.repeat.name -> ApalacheOper.repeat,
       ApalacheInternalOper.selectInSet.name -> ApalacheInternalOper.selectInSet,
       ApalacheInternalOper.selectInFun.name -> ApalacheInternalOper.selectInFun,
       ApalacheInternalOper.storeInSet.name -> ApalacheInternalOper.storeInSet,
@@ -375,6 +376,15 @@ object BuilderCallByName {
       case ApalacheOper.foldSeq =>
         val Seq(f, v, s) = args
         tla.foldSeq(f, v, s)
+      case ApalacheOper.repeat =>
+        val Seq(f, n, x) = args
+        val nEx: TlaEx = n
+        nEx match {
+          case ValEx(TlaInt(n)) =>
+            tla.repeat(f, n, x)
+          // should never happen, for case-completeness
+          case _ => throw new JsonDeserializationError(s"${oper.name} requires an integer argument.")
+        }
       case ApalacheInternalOper.selectInSet =>
         val Seq(x, s) = args
         tla.selectInSet(x, s)
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala
index 380e43075d..2c601465a4 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/StandardLibrary.scala
@@ -67,6 +67,7 @@ object StandardLibrary {
         ("Apalache", "ApaFoldSet") -> ApalacheOper.foldSet,
         ("__apalache_folds", "__ApalacheFoldSet") -> ApalacheOper.foldSet,
         ("Apalache", "ApaFoldSeqLeft") -> ApalacheOper.foldSeq,
+        ("Apalache", "Repeat") -> ApalacheOper.repeat,
         // Variants
         ("Variants", "Variant") -> VariantOper.variant,
         ("Variants", "VariantFilter") -> VariantOper.variantFilter,
diff --git a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
index 50765b5387..780320bf44 100644
--- a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
+++ b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
@@ -810,6 +810,12 @@ class ToEtcExpr(
         mkExRefApp(opsig, Seq(v, variantEx, defaultEx))
 
       // ******************************************** Apalache **************************************************
+      case OperEx(ApalacheOper.repeat, op, bound, base) =>
+        val a = varPool.fresh
+        // ((a, Int) => a, Int, a) => a
+        val opsig = OperT1(Seq(OperT1(Seq(a, IntT1), a), IntT1, a), a)
+        mkExRefApp(opsig, Seq(op, bound, base))
+
       case OperEx(ApalacheOper.mkSeq, len, ctor) =>
         val a = varPool.fresh
         // (Int, (Int => a)) => Seq(a)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala
index bd291c2241..f17344c907 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala
@@ -167,6 +167,19 @@ object ApalacheOper {
     override val precedence: (Int, Int) = (100, 100)
   }
 
+  /**
+   * Repeated applicaiton of an operator.
+   *
+   * The type signature is: `\forall T: Repeat: ((T, Int) => T, Int, T) => T`
+   */
+  object repeat extends ApalacheOper {
+    override def name: String = "Apalache!Repeat"
+
+    override def arity: OperArity = FixedArity(3)
+
+    override val precedence: (Int, Int) = (100, 100)
+  }
+
   /**
    * <p>The operator SetAsFun converts a set of pairs `R` to a function `F`. The function `F` could be expressed as
    * follows:</p>
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
index 3a1cd4b1fd..7ca7451a75 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
@@ -59,6 +59,11 @@ class KeraLanguagePred extends ContextualLanguagePred {
         isOkInContext(letDefs, opName)
           .and(isOkInContext(letDefs, len))
 
+      case OperEx(ApalacheOper.repeat, opName, bound, base) =>
+        isOkInContext(letDefs, opName)
+          .and(isOkInContext(letDefs, bound))
+          .and(isOkInContext(letDefs, base))
+
       case OperEx(oper, args @ _*)
           if oper == TlaSetOper.map || oper == TlaFunOper.funDef || oper == TlaFunOper.recFunDef =>
         val evenArgs = args.zipWithIndex.filter { p => p._2 % 2 == 0 }.map {
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala
index 764794091f..e7a7a8b025 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/signatures/ApalacheOperSignatures.scala
@@ -46,6 +46,12 @@ object ApalacheOperSignatures {
     // (Int, Int => t) => Seq(t)
     val mkSeqSig = signatureMapEntry(mkSeq, { case Seq(IntT1, OperT1(Seq(IntT1), t)) => SeqT1(t) })
 
+    // ((t, Int) => t, Int, t) => t
+    val repeatSig = signatureMapEntry(repeat,
+        {
+          case Seq(OperT1(Seq(IntT1, t), t1), IntT1, t2) if compatible(t, t1) && compatible(t, t2) => t
+        })
+
     // ((a,b) => a, a, Set(b)) => a
     val foldSetSig = signatureMapEntry(foldSet,
         {
@@ -72,6 +78,7 @@ object ApalacheOperSignatures {
         expandSig,
         constCardSig,
         mkSeqSig,
+        repeatSig,
         foldSetSig,
         foldSeqSig,
         setAsFunSig,
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
index b77bd92ece..086eec7375 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala
@@ -36,6 +36,16 @@ trait ApalacheBuilder {
    */
   def gen(n: BigInt, t: TlaType1): TBuilderInstruction = unsafeBuilder.gen(n, t).point[TBuilderInternalState]
 
+  /**
+   * {{{Repeat(F, N, x): t}}}
+   * @param n
+   *   must be a nonnegative constant expression
+   * @param F
+   *   must be an expression of the shape {{{LET Op(i) == ... IN Op}}}
+   */
+  def repeat(F: TBuilderInstruction, n: BigInt, x: TBuilderInstruction): TBuilderInstruction =
+    binaryFromUnsafe(F, x)(unsafeBuilder.repeat(_, n, _))
+
   /**
    * {{{Skolem(ex)}}}
    * @param ex
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
index c42401d7e8..42c63bce5a 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala
@@ -43,6 +43,19 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui
     OperEx(ApalacheOper.gen, mkTlaInt(n))(Typed(t))
   }
 
+  /**
+   * {{{Repeat(F, N, x): t}}}
+   * @param n
+   *   must be a nonnegative constant expression
+   * @param F
+   *   must be an expression of the shape {{{LET Op(i) == ... IN Op}}}
+   */
+  def repeat(F: TlaEx, n: BigInt, x: TlaEx): TlaEx = {
+    if (strict) require(n > 0, s"Expected n to be positive, found $n.")
+    if (strict) require(isNaryPassByName(n = 2)(F), s"Expected F to be a binary operator passed by name, found $F.")
+    buildBySignatureLookup(ApalacheOper.repeat, F, mkTlaInt(n), x)
+  }
+
   /**
    * {{{Skolem(ex)}}}
    * @param ex

From 21127c7990d3b88eed591bda14e48f475a016a16 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 17:01:34 +0200
Subject: [PATCH 21/27] add --timeout-smt

---
 docs/src/apalache/tuning.md                   |  8 ----
 .../apalache/infra/passes/options.scala       |  6 +++
 .../apalache/tla/tooling/opt/CheckCmd.scala   |  7 +++
 test/tla/cli-integration-tests.md             | 12 +++++
 .../forsyte/apalache/tla/bmcmt/Checker.scala  | 15 +++++++
 .../apalache/tla/bmcmt/SeqModelChecker.scala  | 44 ++++++++++++-------
 .../bmcmt/passes/BoundedCheckerPassImpl.scala |  1 +
 .../tla/bmcmt/search/ModelCheckerParams.scala |  8 ++--
 .../tla/bmcmt/search/SearchState.scala        | 16 +++++++
 9 files changed, 90 insertions(+), 27 deletions(-)

diff --git a/docs/src/apalache/tuning.md b/docs/src/apalache/tuning.md
index d3a60c5eeb..22aa77b99a 100644
--- a/docs/src/apalache/tuning.md
+++ b/docs/src/apalache/tuning.md
@@ -22,14 +22,6 @@ The following options are supported:
 `smt.randomSeed=<int>` passes the random seed to `z3` (via `z3`'s parameters
 `sat.random_seed` and `smt.random_seed`).
 
-##  Timeouts
-
-`search.smt.timeout=<seconds>` defines the timeout to the SMT solver in seconds.
-The default value is `0`, which stands for the unbounded timeout.  For instance,
-the timeout is used in the following cases: checking if a transition is enabled,
-checking an invariant, checking for deadlocks. If the solver times out, it
-reports 'UNKNOWN', and the model checker reports a runtime error.
-
 ## Invariant mode
 
 `search.invariant.mode=(before|after)` defines the moment when the invariant is
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala
index 4d676aa3c4..201e26ae1a 100644
--- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala
@@ -162,6 +162,8 @@ object Config {
    *   maximal number of Next steps
    * @param maxError
    *   whether to stop on the first error or to produce up to a given number of counterexamples
+   * @param timeoutSmtSec
+   *   the time limit on SMT queries in seconds
    * @param noDeadLocks
    *   do not check for deadlocks
    * @param smtEncoding
@@ -182,6 +184,7 @@ object Config {
       next: Option[String] = None,
       length: Option[Int] = Some(10),
       maxError: Option[Int] = Some(1),
+      timeoutSmtSec: Option[Int] = Some(0),
       noDeadlocks: Option[Boolean] = Some(false),
       smtEncoding: Option[SMTEncoding] = Some(SMTEncoding.OOPSLA19),
       temporalProps: Option[List[String]] = None,
@@ -660,6 +663,7 @@ object OptionGroup extends LazyLogging {
       discardDisabled: Boolean,
       length: Int,
       maxError: Int,
+      timeoutSmtSec: Int,
       noDeadlocks: Boolean,
       smtEncoding: SMTEncoding,
       tuning: Map[String, String])
@@ -684,11 +688,13 @@ object OptionGroup extends LazyLogging {
         smtEncoding <- checker.smtEncoding.toTry("checker.smtEncoding")
         tuning <- checker.tuning.toTry("checker.tuning")
         maxError <- checker.maxError.toTry("checker.maxError").flatMap(validateMaxError)
+        timeoutSmtSec <- checker.timeoutSmtSec.toTry("checker.timeoutSmtSec")
       } yield Checker(
           algo = algo,
           discardDisabled = discardDisabled,
           length = length,
           maxError = maxError,
+          timeoutSmtSec = timeoutSmtSec,
           noDeadlocks = noDeadlocks,
           smtEncoding = smtEncoding,
           tuning = tuning,
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
index ea957e1bce..5002b88c2e 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
@@ -69,6 +69,12 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
     opt[Boolean](name = "output-traces", description = "save an example trace for each symbolic run, default: false",
         default = false)
 
+  var timeoutSmtSec: Option[Int] =
+    opt[Option[Int]](name = "timeout-smt",
+      description =
+        "limit the duration of a single SMT check query with `n` seconds, default: 0 (unlimited)",
+      default = None)
+
   override def toConfig(): Try[Config.ApalacheConfig] = {
     val loadedTuningOptions = tuningOptionsFile.map(f => loadProperties(f)).getOrElse(Map())
     val combinedTuningOptions = overrideProperties(loadedTuningOptions, tuningOptions.getOrElse("")) ++ Map(
@@ -83,6 +89,7 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
               discardDisabled = discardDisabled,
               noDeadlocks = noDeadlocks,
               maxError = maxError,
+              timeoutSmtSec = timeoutSmtSec,
               view = view,
           ),
           typechecker = cfg.typechecker.copy(
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 6cec251917..ee81bdc10c 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -1752,6 +1752,18 @@ The outcome is: NoError
 EXITCODE: OK
 ```
 
+### simulate Paxos.tla with timeout succeeds
+
+While we cannot rely on an actual timeout happening or not, we can make sure that the option is properly parsed. 
+
+```sh
+$ apalache-mc simulate --timeout-smt=1 --length=10 --inv=Inv Paxos.tla | sed 's/I@.*//'
+...
+The outcome is: NoError
+...
+EXITCODE: OK
+```
+
 ### simulate y2k with --output-traces succeeds
 
 ```sh
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
index 1723856d11..f127c563c9 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
@@ -23,6 +23,8 @@ object Checker {
         Obj("checking_result" -> "Error", "counterexamples" -> counterexamples, "nerrors" -> nerrors)
       case Deadlock(counterexample) =>
         Obj("checking_result" -> "Deadlock", "counterexamples" -> counterexample.toList)
+      case SmtTimeout(nTimeouts) =>
+        Obj("checking_result" -> "SmtTimeout", "ntimeouts" -> nTimeouts)
       case other =>
         Obj("checking_result" -> other.toString())
     }
@@ -60,6 +62,19 @@ object Checker {
     override val isOk: Boolean = true
   }
 
+  /**
+   * The SMT solver reported a timeout. It should still be possible to check other verification conditions.
+   * @param nTimeouts the number of timeouts, normally, just 1.
+   */
+  case class SmtTimeout(nTimeouts: Int) extends CheckerResult {
+    override def toString: String = "SmtTimeout"
+
+    /**
+     * Whether this result shall be reported as success (`true`) or error (`false`).
+     */
+    override val isOk: Boolean = true
+  }
+
   case class Interrupted() extends CheckerResult {
     override def toString: String = "Interrupted"
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
index e7360504ff..da36921b93 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
@@ -94,7 +94,7 @@ class SeqModelChecker[ExecutorContextT](
    */
   private def outputExampleRun(): Unit = {
     logger.info("Constructing an example run")
-    trex.sat(params.smtTimeoutSec) match {
+    trex.sat(params.timeoutSmtSec) match {
       case Some(true) =>
         listeners.foreach(_.onExample(checkerInput.rootModule, trex.decodedExecution(), searchState.nRunsLeft))
       case Some(false) =>
@@ -128,8 +128,8 @@ class SeqModelChecker[ExecutorContextT](
     if (!params.discardDisabled && params.checkForDeadlocks) {
       // We do this check only if all transitions are unconditionally enabled.
       // Otherwise, we should have found it already.
-      logger.info(s"Step %d: checking for deadlocks".format(trex.stepNo))
-      trex.sat(params.smtTimeoutSec) match {
+      logger.info(f"Step ${trex.stepNo}: checking for deadlocks")
+      trex.sat(params.timeoutSmtSec) match {
         case Some(true) => () // OK
 
         case Some(false) =>
@@ -145,7 +145,8 @@ class SeqModelChecker[ExecutorContextT](
           searchState.onResult(Deadlock(counterexample))
 
         case None =>
-          searchState.onResult(RuntimeError())
+          logger.info(f"Step ${trex.stepNo}: checking for deadlocks => TIMEOUT")
+          searchState.onResult(SmtTimeout(1))
       }
     }
 
@@ -204,6 +205,9 @@ class SeqModelChecker[ExecutorContextT](
     val transitionIndices =
       if (params.isRandomSimulation) Random.shuffle(transitions.indices.toList) else transitions.indices
 
+    // keep track of SMT timeouts
+    var nTimeouts = 0
+
     for (no <- transitionIndices) {
       var snapshot: Option[SnapshotT] = None
       if (params.discardDisabled) {
@@ -221,7 +225,7 @@ class SeqModelChecker[ExecutorContextT](
           val assumeSnapshot = trex.snapshot()
           // assume that the transition is fired and check, whether the constraints are satisfiable
           trex.assumeTransition(no)
-          trex.sat(params.smtTimeoutSec) match {
+          trex.sat(params.timeoutSmtSec) match {
             case Some(true) =>
               logger.debug(s"Step ${trex.stepNo}: Transition #$no is enabled")
               // recover to the state before the transition was fired
@@ -263,7 +267,8 @@ class SeqModelChecker[ExecutorContextT](
 
             case None =>
               if (params.isRandomSimulation) {
-                logger.info(s"Step ${trex.stepNo}: Transition #$no enabledness is UNKNOWN; assuming it is disabled")
+                logger.info(s"Step ${trex.stepNo}: Transition #$no => TIMEOUT. Transition ignored.")
+                nTimeouts += 1
               } else {
                 searchState.onResult(RuntimeError())
                 return (Set.empty, Set.empty) // UNKNOWN or timeout
@@ -284,7 +289,13 @@ class SeqModelChecker[ExecutorContextT](
     }
 
     if (trex.preparedTransitionNumbers.isEmpty) {
-      if (params.checkForDeadlocks) {
+      if (nTimeouts > 0 || !params.checkForDeadlocks) {
+        // Either (1) there were timeouts, and we cannot claim to have found a deadlock,
+        // or (2) the user does not care about deadlocks
+        val msg = "All executions are shorter than the provided bound."
+        logger.warn(msg)
+        searchState.onResult(ExecutionsTooShort())
+      } else {
         val counterexample = if (trex.sat(0).contains(true)) {
           val cx = Counterexample(checkerInput.rootModule, trex.decodedExecution(), tla.bool(true))
           notifyOnError(cx, searchState.nFoundErrors)
@@ -295,10 +306,6 @@ class SeqModelChecker[ExecutorContextT](
           None
         }
         searchState.onResult(Deadlock(counterexample))
-      } else {
-        val msg = "All executions are shorter than the provided bound."
-        logger.warn(msg)
-        searchState.onResult(ExecutionsTooShort())
       }
       (Set.empty, Set.empty)
     } else {
@@ -355,7 +362,7 @@ class SeqModelChecker[ExecutorContextT](
           // check the invariant
           trex.assertState(notInv)
 
-          trex.sat(params.smtTimeoutSec) match {
+          trex.sat(params.timeoutSmtSec) match {
             case Some(true) =>
               val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), notInv)
               searchState.onResult(Error(1, Seq(counterexample)))
@@ -369,8 +376,10 @@ class SeqModelChecker[ExecutorContextT](
               logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} holds.")
 
             case None =>
-              // UNKNOWN or timeout
-              searchState.onResult(RuntimeError())
+              // UNKNOWN or timeout. Assume that the invariant holds true, so we can continue.
+              invariantHolds = true
+              logger.info(f"State ${stateNo}: ${kind} invariant ${invNo} => TIMEOUT. Assuming it holds true.")
+              searchState.onResult(SmtTimeout(1))
           }
 
           // rollback the context
@@ -401,7 +410,7 @@ class SeqModelChecker[ExecutorContextT](
         val traceInvApp = applyTraceInv(notInv)
         trex.assertState(traceInvApp)
 
-        trex.sat(params.smtTimeoutSec) match {
+        trex.sat(params.timeoutSmtSec) match {
           case Some(true) =>
             val counterexample = Counterexample(checkerInput.rootModule, trex.decodedExecution(), traceInvApp)
             searchState.onResult(Error(1, Seq(counterexample)))
@@ -415,7 +424,10 @@ class SeqModelChecker[ExecutorContextT](
             invariantHolds = true
 
           case None =>
-            searchState.onResult(RuntimeError())
+            // Timeout. Assume that the invariant holds true, so we can continue.
+            invariantHolds = true
+            logger.info(f"State ${stateNo}: trace invariant ${invNo} => TIMEOUT. Assuming it holds true.")
+            searchState.onResult(SmtTimeout(1))
         }
 
         // rollback the context
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala
index 39cebd8a91..aa2b3bb34a 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/passes/BoundedCheckerPassImpl.scala
@@ -70,6 +70,7 @@ class BoundedCheckerPassImpl @Inject() (
     params.discardDisabled = options.checker.discardDisabled
     params.checkForDeadlocks = !options.checker.noDeadlocks
     params.nMaxErrors = options.checker.maxError
+    params.timeoutSmtSec = options.checker.timeoutSmtSec
     params.smtEncoding = smtEncoding
 
     val smtProfile = options.common.smtprof
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala
index 2c7a052aad..8847475fb0 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/ModelCheckerParams.scala
@@ -68,6 +68,11 @@ class ModelCheckerParams(
    */
   var nMaxErrors: Int = 1
 
+  /**
+   * The limit on a single SMT query. The default value is 0 (unlimited).
+   */
+  var timeoutSmtSec: Int = 0
+
   /**
    * A timeout upon which a transition is split in its own group. This is the minimal timeout. The actual timeout is
    * updated at every step using `search.split.timeout.factor`. In our experiments, small timeouts lead to explosion of
@@ -96,9 +101,6 @@ class ModelCheckerParams(
    */
   def idleTimeoutMs: Long = idleTimeoutSec * 1000
 
-  val smtTimeoutSec: Int =
-    tuningOptions.getOrElse("search.smt.timeout", "0").toInt
-
   /**
    * The SMT encoding to be used.
    */
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala
index 0981dbf004..3a8497250d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/search/SearchState.scala
@@ -18,6 +18,7 @@ class SearchState(params: ModelCheckerParams) {
 
   private var _result: CheckerResult = NoError()
   private var _nFoundErrors: Int = 0
+  private var _nTimeouts: Int = 0
   private val _counterexamples: ListBuffer[Counterexample] = ListBuffer.empty
   private var _nRunsLeft: Int =
     if (params.isRandomSimulation) params.nSimulationRuns else 1
@@ -30,6 +31,14 @@ class SearchState(params: ModelCheckerParams) {
    */
   def nFoundErrors: Int = _nFoundErrors
 
+  /**
+   * Get the number of SMT timeouts that occurred in the search.
+   *
+   * @return
+   *   number of timeouts
+   */
+  def nTimeouts: Int = _nTimeouts
+
   /**
    * Get the number of simulation runs to explore.
    *
@@ -49,6 +58,8 @@ class SearchState(params: ModelCheckerParams) {
       case NoError() =>
         if (_nFoundErrors > 0) {
           Error(_nFoundErrors, _counterexamples.toList)
+        } else if (_nTimeouts > 0) {
+          SmtTimeout(_nTimeouts)
         } else {
           NoError()
         }
@@ -98,6 +109,11 @@ class SearchState(params: ModelCheckerParams) {
           _result = Deadlock(counterexample)
         }
 
+      case SmtTimeout(nTimeouts) =>
+        // we still continue the search, but report incompleteness in [[this.finalResult]].
+        _nTimeouts += nTimeouts
+        _result = NoError()
+
       case _ =>
         _result = result
     }

From 72b48633f9822d8ddc868626279e5818ce59eb41 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 17:06:49 +0200
Subject: [PATCH 22/27] add release notes

---
 .unreleased/features/timeout-smt.md | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 .unreleased/features/timeout-smt.md

diff --git a/.unreleased/features/timeout-smt.md b/.unreleased/features/timeout-smt.md
new file mode 100644
index 0000000000..dd27979cfb
--- /dev/null
+++ b/.unreleased/features/timeout-smt.md
@@ -0,0 +1 @@
+Add `--timeout-smt` to limit SMT queries (#2936)

From f7aeb232442052916bca82b1708b8eb9bc594fa7 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 17:22:37 +0200
Subject: [PATCH 23/27] fix formatting

---
 .../scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala | 5 ++---
 .../main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala   | 3 ++-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
index 5002b88c2e..20a5773436 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/CheckCmd.scala
@@ -71,9 +71,8 @@ class CheckCmd(name: String = "check", description: String = "Check a TLA+ speci
 
   var timeoutSmtSec: Option[Int] =
     opt[Option[Int]](name = "timeout-smt",
-      description =
-        "limit the duration of a single SMT check query with `n` seconds, default: 0 (unlimited)",
-      default = None)
+        description = "limit the duration of a single SMT check query with `n` seconds, default: 0 (unlimited)",
+        default = None)
 
   override def toConfig(): Try[Config.ApalacheConfig] = {
     val loadedTuningOptions = tuningOptionsFile.map(f => loadProperties(f)).getOrElse(Map())
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
index f127c563c9..8bef8a9b07 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Checker.scala
@@ -64,7 +64,8 @@ object Checker {
 
   /**
    * The SMT solver reported a timeout. It should still be possible to check other verification conditions.
-   * @param nTimeouts the number of timeouts, normally, just 1.
+   * @param nTimeouts
+   *   the number of timeouts, normally, just 1.
    */
   case class SmtTimeout(nTimeouts: Int) extends CheckerResult {
     override def toString: String = "SmtTimeout"

From 4930c52367304b89bddb23cfb563c9736c51355f Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 17:49:21 +0200
Subject: [PATCH 24/27] fix the integration tests

---
 test/tla/cli-integration-tests.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index f41ebce01a..cfa06d6d28 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -3904,6 +3904,7 @@ checker {
     smt-encoding {
         type=oopsla-19
     }
+    timeout-smt-sec=0
     tuning {
         "search.outputTraces"="false"
     }

From fb59f3fffaf2a3d461239dbda662f3f664b55f29 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 18:44:12 +0200
Subject: [PATCH 25/27] a first try to fix the release workflow

---
 .github/workflows/README.md           | 10 +++++-----
 .github/workflows/prepare-release.yml |  8 ++++++--
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
index b3226f8407..8b9ff02a67 100644
--- a/.github/workflows/README.md
+++ b/.github/workflows/README.md
@@ -16,15 +16,15 @@
 - Triggered manually.
 - The workflow prepares a release and opens a `[release]` PR.
 - **Requirements**:
-  - A personal API token is required to authenticate the API call that opens the
-    PR.
-    - We use a token belonging to our machine user [@apalache-bot][]. apalache-bot
+  - A personal API token called `APALACHE_BOT_TOKEN` is required to authenticate the API
+    call that opens the PR.
+    - We use a token belonging to our machine user [@coffeeinprogress][]. coffeeinprogress
       creates the PR from their fork of the repo, and they have no permissions in
       this repo itself.
     - Secrets are configured [here][secret-config].
 
-[@apalache-bot]: https://github.com/apalache-bot
-[secret-config]: https://github.com/informalsystems/apalache/settings/secrets/actions
+[@apalache-bot]: https://github.com/coffeeinprogress
+[secret-config]: https://github.com/apalache-mc/apalache/settings/secrets/actions
 
 ## [./release.yml](./release.yml)
 
diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml
index ba77106216..986556aad1 100644
--- a/.github/workflows/prepare-release.yml
+++ b/.github/workflows/prepare-release.yml
@@ -3,7 +3,7 @@ name: prepare-release
 on:
   workflow_dispatch:
     # Allows manually triggering release via
-    # https://github.com/informalsystems/apalache/actions?query=workflow%3A%22Prepare+Release%22
+    # https://github.com/apalache-mc/apalache/actions?query=workflow%3A%22Prepare+Release%22
     inputs:
       release_version:
         description: "Version (leave empty to increment patch version)"
@@ -12,7 +12,7 @@ on:
 
 jobs:
   prepare-release:
-    if: github.repository_owner == 'informalsystems'
+    if: github.repository_owner == 'apalache-mc'
     env:
       RELEASE_VERSION: ${{ github.event.inputs.release_version }}
       # NOTE: We must not use the default GITHUB_TOKEN for auth here,
@@ -22,6 +22,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+      - uses: peter-evans/create-pull-request@v6
+        with:
+          token: ${{ secrets.APALACHE_BOT_TOKEN }}
+          push-to-fork: coffeeinprogress/apalache
       - uses: actions/setup-java@v3
         with:
           distribution: temurin

From a1c3a72107e0b4b9c512eda9a95691925c9f2d63 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 18:45:57 +0200
Subject: [PATCH 26/27] fix the link

---
 .github/workflows/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
index 8b9ff02a67..d8d29ba024 100644
--- a/.github/workflows/README.md
+++ b/.github/workflows/README.md
@@ -23,7 +23,7 @@
       this repo itself.
     - Secrets are configured [here][secret-config].
 
-[@apalache-bot]: https://github.com/coffeeinprogress
+[@@coffeeinprogress]: https://github.com/coffeeinprogress
 [secret-config]: https://github.com/apalache-mc/apalache/settings/secrets/actions
 
 ## [./release.yml](./release.yml)

From e4dc73e3ade6a17e4cc5588b0a34939ebe9bc6cb Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 14 Aug 2024 19:11:45 +0200
Subject: [PATCH 27/27] remove previously added jobs

---
 .github/workflows/prepare-release.yml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml
index 986556aad1..fa189eb981 100644
--- a/.github/workflows/prepare-release.yml
+++ b/.github/workflows/prepare-release.yml
@@ -22,10 +22,6 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: peter-evans/create-pull-request@v6
-        with:
-          token: ${{ secrets.APALACHE_BOT_TOKEN }}
-          push-to-fork: coffeeinprogress/apalache
       - uses: actions/setup-java@v3
         with:
           distribution: temurin