diff --git a/.unreleased/bug-fixes/distinct-on-singleton.md b/.unreleased/bug-fixes/distinct-on-singleton.md
new file mode 100644
index 0000000000..e1aded6fdf
--- /dev/null
+++ 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
index a978d637bb..3e29161038 100644
--- 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