Non-deterministic SMT output by ZipOracle

[thpani]

We some-times permute disjunctions in SMT output:

--- bench.smt	2022-08-31 08:51:17.000000000 +0200
+++ _apalache-out/Termination.tla/2022-09-02T15-49-04_14311296710629792029/log0.smt	2022-09-02 19:12:59.000000000 +0200
 ; [START] Caching equality constraints for a sequence: List(($C$14,$C$246), ($C$13,$C$246), ($C$12,$C$246), ($C$16,$C$246), ($C$11,$C$246), ($C$15,$C$246))
 ; [DONE]  Caching equality constraints
-;; assert (IF (($C$243 = $C$215) ∨ ($C$243 = $C$209) ∨ ($C$243 = $C$233) ∨ ($C$243 = $C$239) ∨ ($C$243 = $C$221) ∨ ($C$243 = $C$227)) THEN ($C$246 = $C$14) ELSE TRUE) ∧ (IF (($C$243 = $C$220) ∨ ($C$243 = $C$208) ∨ ($C$243 = $C$214) ∨ ($C$243 = $C$226) ∨ ($C$243 = $C$238) ∨ ($C$243 = $C$232)) THEN ($C$246 = $C$13) ELSE TRUE) ∧ (IF (($C$243 = $C$225) ∨ ($C$243 = $C$219) ∨ ($C$243 = $C$231) ∨ ($C$243 = $C$207) ∨ ($C$243 = $C$213) ∨ ($C$243 = $C$237)) THEN ($C$246 = $C$12) ELSE TRUE) ∧ (IF (($C$243 = $C$235) ∨ ($C$243 = $C$241) ∨ ($C$243 = $C$223) ∨ ($C$243 = $C$229) ∨ ($C$243 = $C$217) ∨ ($C$243 = $C$211)) THEN ($C$246 = $C$16) ELSE TRUE) ∧ (IF (($C$243 = $C$206) ∨ ($C$243 = $C$236) ∨ ($C$243 = $C$230) ∨ ($C$243 = $C$218) ∨ ($C$243 = $C$212) ∨ ($C$243 = $C$224)) THEN ($C$246 = $C$11) ELSE TRUE) ∧ (IF (($C$243 = $C$240) ∨ ($C$243 = $C$216) ∨ ($C$243 = $C$222) ∨ ($C$243 = $C$228) ∨ ($C$243 = $C$210) ∨ ($C$243 = $C$234)) THEN ($C$246 = $C$15) ELSE TRUE)
-(assert (and (ite (or (= $C$243 $C$215)
+;; assert (IF (($C$243 = $C$233) ∨ ($C$243 = $C$209) ∨ ($C$243 = $C$239) ∨ ($C$243 = $C$215) ∨ ($C$243 = $C$227) ∨ ($C$243 = $C$221)) THEN ($C$246 = $C$14) ELSE TRUE) ∧ (IF (($C$243 = $C$232) ∨ ($C$243 = $C$220) ∨ ($C$243 = $C$208) ∨ ($C$243 = $C$226) ∨ ($C$243 = $C$238) ∨ ($C$243 = $C$214)) THEN ($C$246 = $C$13) ELSE TRUE) ∧ (IF (($C$243 = $C$237) ∨ ($C$243 = $C$219) ∨ ($C$243 = $C$207) ∨ ($C$243 = $C$213) ∨ ($C$243 = $C$225) ∨ ($C$243 = $C$231)) THEN ($C$246 = $C$12) ELSE TRUE) ∧ (IF (($C$243 = $C$217) ∨ ($C$243 = $C$229) ∨ ($C$243 = $C$241) ∨ ($C$243 = $C$235) ∨ ($C$243 = $C$223) ∨ ($C$243 = $C$211)) THEN ($C$246 = $C$16) ELSE TRUE) ∧ (IF (($C$243 = $C$218) ∨ ($C$243 = $C$212) ∨ ($C$243 = $C$236) ∨ ($C$243 = $C$224) ∨ ($C$243 = $C$230) ∨ ($C$243 = $C$206)) THEN ($C$246 = $C$11) ELSE TRUE) ∧ (IF (($C$243 = $C$228) ∨ ($C$243 = $C$222) ∨ ($C$243 = $C$240) ∨ ($C$243 = $C$216) ∨ ($C$243 = $C$234) ∨ ($C$243 = $C$210)) THEN ($C$246 = $C$15) ELSE TRUE)
+(assert (and (ite (or (= $C$243 $C$233)
               (= $C$243 $C$209)
-              (= $C$243 $C$233)
               (= $C$243 $C$239)
-              (= $C$243 $C$221)
-              (= $C$243 $C$227))
+              (= $C$243 $C$215)
+              (= $C$243 $C$227)
+              (= $C$243 $C$221))
           (= $C$246 $C$14)
           true)
-     (ite (or (= $C$243 $C$220)
+     (ite (or (= $C$243 $C$232)
+              (= $C$243 $C$220)
               (= $C$243 $C$208)
-              (= $C$243 $C$214)
               (= $C$243 $C$226)
               (= $C$243 $C$238)
-              (= $C$243 $C$232))
+              (= $C$243 $C$214))
           (= $C$246 $C$13)
           true)

Originally posted by @thpani in #2120 (comment)

[thpani]

Thanks to @Kukovec and @konnov for helping debug to identify this line:

https://github.com/informalsystems/apalache/blob/a2e967e31684f958af0492a5387f21c6abac1b11/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala#L129