From 2b4b70a6ca3aa5f10e0dc079b5304a4e56f7c13c Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 15 Aug 2024 01:02:57 +0200
Subject: [PATCH 01/11] changing paths

---
 .github/workflows/README.md              |  2 +-
 docs/src/apalache/installation/docker.md | 22 +++++++++++-----------
 script/run-docker.sh                     |  4 ++--
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/.github/workflows/README.md b/.github/workflows/README.md
index d8d29ba024..49339e90ce 100644
--- a/.github/workflows/README.md
+++ b/.github/workflows/README.md
@@ -9,7 +9,7 @@
 
 - Triggered by pull requests into `main`.
 - Used for any artifacts that we deploy into production environments. Currently,
-  this only consists of our website at https://apalache.informal.systems.
+  this only consists of our website at https://apalache-mc.org.
 
 ## [./prepare-release.yml](./prepare-release.yml)
 
diff --git a/docs/src/apalache/installation/docker.md b/docs/src/apalache/installation/docker.md
index d5eea19e76..c43bfbea58 100644
--- a/docs/src/apalache/installation/docker.md
+++ b/docs/src/apalache/installation/docker.md
@@ -14,7 +14,7 @@ suitable JVM, and the container supplies this. However, you must already have
 To get the latest Apalache image, issue the command:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache
+docker pull ghcr.io/apalache-mc/apalache
 ```
 
 ## Running the docker image
@@ -22,7 +22,7 @@ docker pull ghcr.io/informalsystems/apalache
 To run an Apalache image, issue the command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache <args>
 ```
 
 The following docker parameters are used:
@@ -38,8 +38,8 @@ The following docker parameters are used:
 
   When using SELinux, you might have to use the modified form of `-v` option:
     `-v <your-spec-directory>:/var/apalache:z`
-- `informalsystems/apalache` is the APALACHE docker image name. By default, the `latest` stable
-  version is used; you can also refer to a specific tool version, e.g., `informalsystems/apalache:0.6.0` or `informalsystems/apalache:main`
+- `apalache-mc/apalache` is the APALACHE docker image name. By default, the `latest` stable
+  version is used; you can also refer to a specific tool version, e.g., `apalache-mc/apalache:0.6.0` or `apalache-mc/apalache:main`
 - `<args>` are the tool arguments as described in [Running the Tool](../running.md).
 
 We provide a convenience wrapper for this docker command in
@@ -67,11 +67,11 @@ Apalache in docker while sharing the working directory:
 
 ###### using the latest stable
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache'
 
 ###### using the latest main
 
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 ## Using the development branch of Apalache
@@ -82,25 +82,25 @@ branch for a report of the newest features. Since we cut releases weekly, you
 should have access to all the latest features in the last week by using the
 `latest` tag. However, if you wish to use the very latest developments as they
 are added throughout the week, you can run the image with the `main` tag: just
-type `ghcr.io/informalsystems/apalache:main` instead of
-`ghcr.io/informalsystems/apalache` everywhere.
+type `ghcr.io/apalache-mc/apalache:main` instead of
+`ghcr.io/apalache-mc/apalache` everywhere.
 
 Do not forget to pull the docker image from time to time:
 
 ```bash
-docker pull ghcr.io/informalsystems/apalache:main
+docker pull ghcr.io/apalache-mc/apalache:main
 ```
 
 Run it with the following command:
 
 ```bash
-$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/informalsystems/apalache:main <args>
+$ docker run --rm -v <your-spec-directory>:/var/apalache ghcr.io/apalache-mc/apalache:main <args>
 ```
 
 To create an alias pointing to the `main` version:
 
 ```bash
-$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/informalsystems/apalache:main'
+$ alias apalache='docker run --rm -v $(pwd):/var/apalache ghcr.io/apalache-mc/apalache:main'
 ```
 
 [changelog]: https://github.com/informalsystems/apalache/blob/main/CHANGES.md
diff --git a/script/run-docker.sh b/script/run-docker.sh
index 05d3df4c8b..4f8a094ffc 100755
--- a/script/run-docker.sh
+++ b/script/run-docker.sh
@@ -14,9 +14,9 @@ if [ -z "$APALACHE_TAG" ]
 then
     >&2 echo "# No docker image supplied. Defaulting to '$default_tag'"
     >&2 echo "# To run a specific docker tag set APALACHE_TAG."
-    img="ghcr.io/informalsystems/apalache:${default_tag}"
+    img="ghcr.io/apalache-mc/apalache:${default_tag}"
 else
-    img="ghcr.io/informalsystems/apalache:${APALACHE_TAG}"
+    img="ghcr.io/apalache-mc/apalache:${APALACHE_TAG}"
 fi
 
 # TODO Programmatically generate envars to expose here

From 4ef62e9116d6923686aaff80c084016bd596ec19 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 15 Aug 2024 10:37:28 +0200
Subject: [PATCH 02/11] update the build data

---
 build.sbt | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/build.sbt b/build.sbt
index 83145fae79..5d668fedf7 100644
--- a/build.sbt
+++ b/build.sbt
@@ -8,11 +8,11 @@ import scala.sys.process._
 ///////////////////////////
 
 name := "apalache"
-maintainer := "apalache@informal.org"
+maintainer := "apalache@konnov.phd"
 
 // See https://www.scala-sbt.org/1.x/docs/Multi-Project.html#Build-wide+settings
-ThisBuild / organizationName := "Informal Systems Inc."
-ThisBuild / organizationHomepage := Some(url("https://informal.systems"))
+ThisBuild / organizationName := "Apalache Development Team"
+ThisBuild / organizationHomepage := Some(url("https://apalache-mc.org"))
 ThisBuild / licenses += "Apache 2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0")
 
 // We store the version in a bare file to make accessing and updating the version trivial
@@ -351,7 +351,7 @@ lazy val root = (project in file("."))
         log.info(s"Unpacking package ${pkg} to ${target_dir}")
         // send outputs directly to std{err,out} instead of logging here
         // to avoid misleading logging output from tar
-        // See https://github.com/informalsystems/apalache/pull/1382
+        // See https://github.com/apalache-mc/apalache/pull/1382
         (s"tar zxvf ${pkg} -C ${target_dir}" !)
         log.info(s"Symlinking ${current_pkg} -> ${unzipped}")
         if (current_pkg.exists) {
@@ -369,7 +369,7 @@ lazy val root = (project in file("."))
 docker / imageNames := {
   val img: String => ImageName = s =>
     ImageName(
-        namespace = Some("ghcr.io/informalsystems"),
+        namespace = Some("ghcr.io/apalache-mc"),
         repository = name.value,
         tag = Some(s),
     )
@@ -425,7 +425,7 @@ lazy val versionFile = settingKey[File]("Location of the file tracking the proje
 // These tasks are used in our bespoke release pipeline
 // TODO(shon): Once we've changed our packaging to conform to more standard SBT structures and practices,
 // we should consider moving to a release pipeline based around sbt-release.
-// See https://github.com/informalsystems/apalache/issues/1248
+// See https://github.com/apalache-mc/apalache/issues/1248
 
 lazy val printVersion = taskKey[Unit]("Print the current version")
 printVersion := {

From eb78dcdf21266b19ede1c3362373dd3471197457 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 15 Aug 2024 10:45:39 +0200
Subject: [PATCH 03/11] switch to the azul docker image

---
 build.sbt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.sbt b/build.sbt
index 5d668fedf7..0202123960 100644
--- a/build.sbt
+++ b/build.sbt
@@ -391,7 +391,7 @@ docker / dockerfile := {
   val readme = rootDir / "README.md"
 
   new Dockerfile {
-    from("eclipse-temurin:17")
+    from("azul/zulu-openjdk:17-latest")
 
     workDir(dwd)
 

From 9ab5a6b4e1aee072274cd61ca796deec1f938f76 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 15 Aug 2024 12:03:05 +0200
Subject: [PATCH 04/11] use test instead of test-coverage

---
 .github/workflows/main.yml | 7 +------
 Makefile                   | 3 ++-
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 5a95199b64..20b48cdeb6 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -101,12 +101,7 @@ jobs:
         # See https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-an-environment-variable
         run: echo "APALACHE_HOME=$GITHUB_WORKSPACE" >> $GITHUB_ENV
       - name: Build and Unit Test
-        run: make test-coverage
-      - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@v2
-        with:
-          # See https://app.codecov.io/gh/informalsystems/apalache/
-          token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos
+        run: make test
       - name: Cleanup before cache
         # See https://www.scala-sbt.org/1.x/docs/GitHub-Actions-with-sbt.html#Caching
         shell: bash
diff --git a/Makefile b/Makefile
index 0058403306..16ed465722 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,8 @@ compile-strict: export APALACHE_FATAL_WARNINGS=true
 compile-strict:
 	sbt Test/compile compile
 
-# Run tests with scoverage report
+# Run tests with scoverage report.
+# This target is not used in the CI anymore. It needs additional devops work to re-enable it.
 test-coverage:
 	sbt coverage test coverageAggregate
 

From 0a1e7541edee776a7b63769946b69b94a9d90b41 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Thu, 15 Aug 2024 15:22:41 +0000
Subject: [PATCH 05/11] Update scalacheck to 1.18.0

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

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index d8af95aa45..c3329635ad 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -53,7 +53,7 @@ object Dependencies {
   object TestDeps {
     // Libraries
     val junit = "junit" % "junit" % "4.13.2" % Test
-    val scalacheck = "org.scalacheck" %% "scalacheck" % "1.17.1" % Test
+    val scalacheck = "org.scalacheck" %% "scalacheck" % "1.18.0" % Test
     val easymock = "org.easymock" % "easymock" % "5.4.0" % Test
 
     val scalaTestVersion = "3.2.15"

From b0eb4d868e9153e11c42a45a12324ce537f8e2fd Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 16 Aug 2024 11:37:36 +0200
Subject: [PATCH 06/11] revert to Temurin

---
 build.sbt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/build.sbt b/build.sbt
index 0202123960..e3a78b4616 100644
--- a/build.sbt
+++ b/build.sbt
@@ -391,7 +391,7 @@ docker / dockerfile := {
   val readme = rootDir / "README.md"
 
   new Dockerfile {
-    from("azul/zulu-openjdk:17-latest")
+    from("eclipse-temurin:17")
 
     workDir(dwd)
 
@@ -406,7 +406,7 @@ docker / dockerfile := {
 
     // We need sudo to run apalache using the user (created in the entrypoint script)
     run("apt", "update")
-    run("apt", "install", "sudo")
+    run("apt", "install", "-y", "sudo")
 
     entryPoint("/opt/apalache/bin/run-in-docker-container")
   }

From 31909931ef06988f2023d5793ee21f3e5b813729 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 16 Aug 2024 19:51:43 +0200
Subject: [PATCH 07/11] enable docker tests

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

diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 5a95199b64..43f314e500 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -166,8 +166,6 @@ 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 1538dd982f59918b9adb279f4ae38667f402f810 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Fri, 16 Aug 2024 10:43:55 +0200
Subject: [PATCH 08/11] Rewrite for set membership of the powerset of a record
 where the record has infinite co-domains.

Simplified real-world scenario:
```tla
EXTENDS Integers

VARIABLE
  \* @type: Set({ p: (Int) });
  v

TypeOK ==
  v \in SUBSET [ p: Int ]

Init ==
  v = { [p |-> 42] }

Next ==
  UNCHANGED v
```

Apalache Error:
```sh
$ apalache-mc check --inv=TypeOK APARecSub.tla
[...]
Input error (see the manual): Found a set map over an infinite set of CellTFrom(Int). Not supported.
```

Rewrite:
```tla
S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T
```

Related commits, issues, PRs:
* 625a1645e75a910d43759c36ad8a06291ebc55b3
* 785e26925a45b077e14cf79f31f834e0c0919639

* https://github.com/apalache-mc/apalache/issues/723
* https://github.com/apalache-mc/apalache/issues/1627
* https://github.com/apalache-mc/apalache/issues/2762

* https://github.com/apalache-mc/apalache/pull/1453
* https://github.com/apalache-mc/apalache/pull/1629

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
---
 .unreleased/features/rewrite.md               |  1 +
 .../apalache/tla/pp/ExprOptimizer.scala       | 28 +++++++
 .../apalache/tla/pp/TestExprOptimizer.scala   | 80 ++++++++++++++++++-
 3 files changed, 108 insertions(+), 1 deletion(-)
 create mode 100644 .unreleased/features/rewrite.md

diff --git a/.unreleased/features/rewrite.md b/.unreleased/features/rewrite.md
new file mode 100644
index 0000000000..00fb95d91b
--- /dev/null
+++ b/.unreleased/features/rewrite.md
@@ -0,0 +1 @@
+Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
\ No newline at end of file
diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala
index e85d215f85..9faa5d1b68 100644
--- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala
+++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala
@@ -97,6 +97,34 @@ class ExprOptimizer(nameGen: UniqueNameGenerator, tracker: TransformationTracker
         }
         apply(tla.and(domEq +: fieldsEq: _*).as(b))
       }
+
+    // S ∈ SUBSET { ["a" ↦ x] : x ∈ T }
+    case memEx @ OperEx(TlaSetOper.in, setRec,
+            OperEx(TlaSetOper.powerset,
+                OperEx(TlaSetOper.map, OperEx(TlaFunOper.rec, fieldsAndValues @ _*), varsAndSets @ _*)))
+        if fieldsAndValues.length == varsAndSets.length =>
+      val (fields, values) = TlaOper.deinterleave(fieldsAndValues)
+      val (vars, sets) = TlaOper.deinterleave(varsAndSets)
+      assert(fields.length == vars.length)
+      if (values.zip(vars).exists(p => p._1 != p._2)) {
+        // The set has a more general form: { [f_1 |-> e_1, ..., f_k |-> e_k]: x_1 \in S_1, ..., x_k \in S_k }, where
+        //   e_1, ..., e_k are expressions over x_1, ..., x_k.
+        // We do not know how to optimize it.
+        memEx
+      } else {
+        val strSetT = SetT1(StrT1)
+        val b = BoolT1
+
+        val domType = getElemType(setRec)
+        val r = tla.name(nameGen.newName()).as(domType)
+
+        val domEq = tla.eql(tla.dom(r).as(SetT1(domType)), tla.enumSet(fields: _*).as(strSetT)).as(b)
+
+        val fieldsEq = fields.zip(values.zip(sets)).map { case (key, (value, set)) =>
+          tla.in(tla.appFun(r, key).as(value.typeTag.asTlaType1()), set).as(b)
+        }
+        apply(tla.forall(r, setRec, tla.and(domEq +: fieldsEq: _*).as(b)).as(b))
+      }
   }
 
   /**
diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
index 5f13923734..a38e77fefc 100644
--- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
+++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala
@@ -87,22 +87,100 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach {
 
   // An optimization for set membership over sets of records. Note that this is the standard form produced by Keramelizer.
   test("""r \in { [a |-> x, b |-> y]: x \in S, y \in T } becomes DOMAIN r = { "a", "b" } /\ r.a \in S /\ r.b \in T""") {
+    // ... [a |-> x, b |-> y] ...
     val recT = RecT1("a" -> IntT1, "b" -> IntT1)
-    val recSetT = SetT1(recT)
+    // ... x \in S, y \in T ...
     val record =
       enumFun(str("a"), name("x").as(intT), str("b"), name("y").as(intT)).as(recT)
+    // ... S ...
     val S = name("S").as(intSetT)
+    // ... T ...
     val T = name("T").as(intSetT)
+    // { ... }
+    val recSetT = SetT1(recT)
     val recordSet = map(record, name("x").as(intT), S, name("y").as(intT), T).as(recSetT)
+    // r ...
     val r = name("r").as(recT)
+    // ... \in ...
     val input = in(r, recordSet).as(boolT)
 
+    // ~~>
+
+    // DOMAIN r = { "a", "b" }
     val strSetT = SetT1(StrT1)
     val domEq = eql(dom(r).as(strSetT), enumSet(str("a"), str("b")).as(strSetT)).as(boolT)
+    // r.a \in S
     val memA = in(appFun(r, str("a")).as(intT), S).as(boolT)
+    // r.b \in T
     val memB = in(appFun(r, str("b")).as(intT), T).as(boolT)
+    // ... /\ ... /\ ...
     val expected = and(domEq, memA, memB).as(boolT)
     val output = optimizer.apply(input)
+
+    assert(expected == output)
+  }
+
+  // An optimization for set membership of the powerset of a record where the record has infinite co-domains.
+  test("""S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T""") {
+
+    // ... { [a |-> x] : x \in T } ...
+    val recT = RecT1("a" -> IntT1)
+    val record =
+      enumFun(str("a"), name("x").as(intT)).as(recT)
+    val T = name("T").as(intSetT)
+    val recSetT = SetT1(recT)
+    val recordSet = map(record, name("x").as(intT), T).as(recSetT)
+
+    // ... SUBSET ...
+    val powSetT = powSet(recordSet).as(recSetT)
+
+    // S ...
+    val s = name("S").as(recSetT)
+
+    // ... \in ...
+    val input = in(s, powSetT).as(boolT)
+    val output = optimizer.apply(input)
+
+    // ~~>
+
+    // DOMAIN r = { "a" }
+    val r = name("t_1").as(recT)
+    val strSetT = SetT1(StrT1)
+    val domEq = eql(dom(r).as(strSetT), enumSet(str("a")).as(strSetT)).as(boolT)
+
+    // r.a \in T
+    val memA = in(appFun(r, str("a")).as(intT), T).as(boolT)
+
+    // ... /\ ...
+    val conjunct = and(domEq, memA).as(boolT)
+
+    // \A ...
+    val expected = forall(r, s, conjunct).as(boolT)
+
+    assert(expected == output)
+  }
+
+  test("""S \in SUBSET [a : T, b : U] ~~> \A r \in S: DOMAIN r = { "a", "b" } /\ r.a \in T /\ r.b \in U""") {
+    val recT = RecT1("a" -> IntT1, "b" -> IntT1)
+    val record =
+      enumFun(str("a"), name("x").as(intT), str("b"), name("y").as(intT)).as(recT)
+    val T = name("T").as(intSetT)
+    val U = name("U").as(intSetT)
+    val recSetT = SetT1(recT)
+    val recordSet = map(record, name("x").as(intT), T, name("y").as(intT), U).as(recSetT)
+    val powSetT = powSet(recordSet).as(recSetT)
+    val s = name("S").as(recSetT)
+    val input = in(s, powSetT).as(boolT)
+    val output = optimizer.apply(input)
+
+    val r = name("t_1").as(recT)
+    val strSetT = SetT1(StrT1)
+    val domEq = eql(dom(r).as(strSetT), enumSet(str("a"), str("b")).as(strSetT)).as(boolT)
+    val memA = in(appFun(r, str("a")).as(intT), T).as(boolT)
+    val memB = in(appFun(r, str("b")).as(intT), U).as(boolT)
+    val conjunct = and(domEq, memA, memB).as(boolT)
+    val expected = forall(r, s, conjunct).as(boolT)
+
     assert(expected == output)
   }
 

From 1a4229a4c22aff04b1cf3d7dc75f5c374ea3dbd8 Mon Sep 17 00:00:00 2001
From: Scala Steward <scala_steward@virtuslab.com>
Date: Sat, 17 Aug 2024 14:14:55 +0000
Subject: [PATCH 09/11] Update logback-classic, logback-core to 1.5.7

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

diff --git a/project/Dependencies.scala b/project/Dependencies.scala
index 8014769576..ed98809c61 100644
--- a/project/Dependencies.scala
+++ b/project/Dependencies.scala
@@ -12,7 +12,7 @@ object Dependencies {
 
   object Deps {
     // Versions
-    lazy val logbackVersion = "1.5.6"
+    lazy val logbackVersion = "1.5.7"
     lazy val clistVersion = "3.5.1"
 
     // Libraries

From 13c39f5ef9fde86277635a8fae1fc394313c26f6 Mon Sep 17 00:00:00 2001
From: konnov <github@actions.ci>
Date: Sat, 17 Aug 2024 15:52:48 +0000
Subject: [PATCH 10/11] [release] 0.45.0

---
 RELEASE.md | 7 +++++++
 VERSION    | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 RELEASE.md

diff --git a/RELEASE.md b/RELEASE.md
new file mode 100644
index 0000000000..f5d281c853
--- /dev/null
+++ b/RELEASE.md
@@ -0,0 +1,7 @@
+## 0.45.0 - 2024-08-17
+
+### Features
+
+- Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
+- Translate Quint's generate into `Apalache!Gen` (#2916)
+- Add `--timeout-smt` to limit SMT queries (#2936)
diff --git a/VERSION b/VERSION
index 93722f80fa..bcce5d06b8 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-0.44.12-SNAPSHOT
+0.45.0

From 553ff28f7c5a5072f35127cda4a83696f1d03db9 Mon Sep 17 00:00:00 2001
From: konnov <github@actions.ci>
Date: Sat, 17 Aug 2024 15:52:56 +0000
Subject: [PATCH 11/11] Bump version to 0.45.1-SNAPSHOT

---
 .unreleased/features/rewrite.md            | 1 -
 .unreleased/features/timeout-smt.md        | 1 -
 .unreleased/features/translate-generate.md | 1 -
 CHANGES.md                                 | 8 ++++++++
 RELEASE.md                                 | 7 -------
 VERSION                                    | 2 +-
 6 files changed, 9 insertions(+), 11 deletions(-)
 delete mode 100644 .unreleased/features/rewrite.md
 delete mode 100644 .unreleased/features/timeout-smt.md
 delete mode 100644 .unreleased/features/translate-generate.md
 delete mode 100644 RELEASE.md

diff --git a/.unreleased/features/rewrite.md b/.unreleased/features/rewrite.md
deleted file mode 100644
index 00fb95d91b..0000000000
--- a/.unreleased/features/rewrite.md
+++ /dev/null
@@ -1 +0,0 @@
-Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
\ No newline at end of file
diff --git a/.unreleased/features/timeout-smt.md b/.unreleased/features/timeout-smt.md
deleted file mode 100644
index dd27979cfb..0000000000
--- a/.unreleased/features/timeout-smt.md
+++ /dev/null
@@ -1 +0,0 @@
-Add `--timeout-smt` to limit SMT queries (#2936)
diff --git a/.unreleased/features/translate-generate.md b/.unreleased/features/translate-generate.md
deleted file mode 100644
index 326f24450d..0000000000
--- a/.unreleased/features/translate-generate.md
+++ /dev/null
@@ -1 +0,0 @@
-Translate Quint's generate into `Apalache!Gen` (#2916)
diff --git a/CHANGES.md b/CHANGES.md
index e370b63d49..e523bc2b40 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,14 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
  
+## 0.45.0 - 2024-08-17
+
+### Features
+
+- Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
+- Translate Quint's generate into `Apalache!Gen` (#2916)
+- Add `--timeout-smt` to limit SMT queries (#2936)
+
 ## 0.44.11 - 2024-05-06
 
 ### Features
diff --git a/RELEASE.md b/RELEASE.md
deleted file mode 100644
index f5d281c853..0000000000
--- a/RELEASE.md
+++ /dev/null
@@ -1,7 +0,0 @@
-## 0.45.0 - 2024-08-17
-
-### Features
-
-- Handle expressions such as  S \in SUBSET [ a : Int ]  by rewriting the expression into  \A r \in S: DOMAIN r = {"a"} /\ r.a \in Int
-- Translate Quint's generate into `Apalache!Gen` (#2916)
-- Add `--timeout-smt` to limit SMT queries (#2936)
diff --git a/VERSION b/VERSION
index bcce5d06b8..630d1052de 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-0.45.0
+0.45.1-SNAPSHOT