diff --git a/.unreleased/bug-fixes/sort-zip-oracle.md b/.unreleased/bug-fixes/sort-zip-oracle.md
new file mode 100644
index 0000000000..2f611fc487
--- /dev/null
+++ b/.unreleased/bug-fixes/sort-zip-oracle.md
@@ -0,0 +1 @@
+Sort SMT disjuncts generated by `ZipOracle`, see #2149 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
index 08c14783bc..2ab7c94ff4 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
+++ b/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)
     }
 
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
index 882d2e5453..7e3ea45566 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
+++ b/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 = {