Sort disjuncts generated by ZipOracle (#2149)

.unreleased/bug-fixes/sort-zip-oracle.md

@@ -0,0 +1 @@
+Sort SMT disjuncts generated by `ZipOracle`, see #2149 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala

@@ -126,7 +126,10 @@ class CherryPick(rewriter: SymbStateRewriter) {
     // This optimization gives us a 20% speed up on a small set of benchmarks.
     val groups = elems.indices.groupBy(elems(_))
     if (groups.size < elems.size) {
-      val zipOracle = new ZipOracle(oracle, groups.values.toList.map(is => Set(is: _*)))
+      val zipOracle = new ZipOracle(oracle,
+          // Sort indices, it determines the order of SMT disjuncts generated by the oracle;
+          // See https://github.com/informalsystems/apalache/issues/2120
+          groups.values.toSeq.map(_.sorted))
       return pickByOracle(state, zipOracle, groups.keys.toSeq, elseAssert)
     }
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala

@@ -15,9 +15,11 @@ import at.forsyte.apalache.tla.lir.{BoolT1, TlaEx}
  * @param backOracle
  *   the background oracle whose values are grouped together
  * @param groups
- *   a list of groups over the indices of the background oracle
+ *   A list of groups over the indices of the background oracle. Indices within each group must be sorted, as the
+ *   sorting determines the order of generated SMT constraints; see
+ *   https://github.com/informalsystems/apalache/issues/2120.
  */
-class ZipOracle(backOracle: Oracle, groups: List[Set[Int]]) extends Oracle {
+class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle {
   override def size: Int = groups.size
 
   override def whenEqualTo(state: SymbState, index: Int): TlaEx = {