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..a577b66f48 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 @@ -106,6 +106,10 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach { 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""") { + } + // optimizations for set cardinalities test("""Cardinality(S) = 0 becomes S = {}""") {