Merge branch 'main' into igor/vcgen-source

apalache-mc · Oct 4, 2024 · 51c423a · 51c423a
2 parents 35b826b + dd37ffa
commit 51c423a
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 8 deletions.
diff --git a/.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md b/.unreleased/bug-fixes/BogusSafetyViolationSubsetNat.md
diff --git a/.unreleased/bug-fixes/distinct-on-singleton.md b/.unreleased/bug-fixes/distinct-on-singleton.md
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,6 +1,19 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
 
+## 0.47.0 - 2024-10-02
+
+### Breaking changes
+
+- Downgrade z3 to 4.12.6, due to instability of 4.13.0
+
+## 0.46.2 - 2024-10-02
+
+### Bug fixes
+
+- Do not produce `(distinct ...)` for singletons, see #3005
+- Show note that expression is unsupported instead of reporting a counterexample claiming that e.g. `{42} \in SUBSET Nat` is false, see #2690
+
 ## 0.46.1 - 2024-09-24
 
 ### Features

diff --git a/VERSION b/VERSION
@@ -1 +1 @@
-0.46.2-SNAPSHOT
+0.47.1-SNAPSHOT
diff --git a/project/Dependencies.scala b/project/Dependencies.scala
@@ -34,9 +34,9 @@ object Dependencies {
     val slf4j = "org.slf4j" % "slf4j-api" % "2.0.16"
     val shapeless = "com.chuusai" %% "shapeless" % "2.3.12"
     val tla2tools = "org.lamport" % "tla2tools" % "1.7.0-SNAPSHOT"
-    val ujson = "com.lihaoyi" %% "ujson" % "4.0.1"
-    val upickle = "com.lihaoyi" %% "upickle" % "4.0.1"
-    val z3 = "tools.aqua" % "z3-turnkey" % "4.13.0"
+    val ujson = "com.lihaoyi" %% "ujson" % "4.0.2"
+    val upickle = "com.lihaoyi" %% "upickle" % "4.0.2"
+    val z3 = "tools.aqua" % "z3-turnkey" % "4.12.6"
     val zio = "dev.zio" %% "zio" % zioVersion
     // Keep up to sync with version in plugins.sbt
     val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided"

diff --git a/project/plugins.sbt b/project/plugins.sbt
@@ -5,13 +5,13 @@ addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.2.0")
 // https://github.com/marcuslonnberg/sbt-docker
 addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0")
 // https://github.com/scoverage/sbt-scoverage
-addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.2.0")
+addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.2.1")
 // https://github.com/sbt/sbt-buildinfo
 addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.12.0")
 // https://github.com/sbt/sbt-native-packager
 addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.10.4")
 // https://scalacenter.github.io/scalafix/docs/users/installation.html
-addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.12.1")
+addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.13.0")
 // https://scalapb.github.io/zio-grpc/docs/installation
 addSbtPlugin("com.thesamet" % "sbt-protoc" % "1.0.6")
 // https://github.com/sbt/sbt-unidoc