Merge branch 'main' into update/ujson-4.0.2

apalache-mc · Oct 1, 2024 · 3427b0f · 3427b0f
2 parents 11de4fe + 97263b5
commit 3427b0f
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 7 deletions.
diff --git a/.unreleased/bug-fixes/distinct-on-singleton.md b/.unreleased/bug-fixes/distinct-on-singleton.md
@@ -0,0 +1 @@
+Do not produce `(distinct ...)` for singletons, see #3005
diff --git a/project/plugins.sbt b/project/plugins.sbt
@@ -11,7 +11,7 @@ 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

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -765,12 +765,17 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
         (z3context.mkNot(eq.asInstanceOf[BoolExpr]).asInstanceOf[ExprSort], 1 + n)
 
       case OperEx(ApalacheInternalOper.distinct, args @ _*) =>
-        val (es, ns) = (args.map(toExpr)).unzip
-        val distinct = z3context.mkDistinct(es: _*)
-        (distinct.asInstanceOf[ExprSort],
-            ns.foldLeft(1L) {
-              _ + _
-            })
+        if (args.length < 2) {
+          // Produce true for a singleton set or an empty set. Otherwise, we cannot replay the SMT log in CVC5.
+          (z3context.mkTrue().asInstanceOf[ExprSort], 1)
+        } else {
+          val (es, ns) = (args.map(toExpr)).unzip
+          val distinct = z3context.mkDistinct(es: _*)
+          (distinct.asInstanceOf[ExprSort],
+              ns.foldLeft(1L) {
+                _ + _
+              })
+        }
 
       case OperEx(TlaBoolOper.and, args @ _*) =>
         val (es, ns) = (args.map(toExpr)).unzip