Merge pull request #3005 from apalache-mc/igor/distinct2964

produce true on distinct for less than 2 elements
apalache-mc · Sep 30, 2024 · 2734569 · 2734569
2 parents 169d142 + 7db8fa4
commit 2734569
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 6 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/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