Sort disjuncts generated by ZipOracle

[thpani]

Make SMT output deterministic by fixing the order of SMT constraints generated by ZipOracle.
Fixes #2150

Tested across 14 identical runs of Apalache.

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entries added to ./unreleased/ for any new functionality

[codecov-commenter]

Codecov Report

Merging #2149 (396fb41) into main (970ab4d) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff           @@
##             main    #2149   +/-   ##
=======================================
  Coverage   77.14%   77.15%           
=======================================
  Files         423      423           
  Lines       13845    13846    +1     
  Branches     1879     1898   +19     
=======================================
+ Hits        10681    10683    +2     
+ Misses       3164     3163    -1     

Impacted Files	Coverage Δ
...rsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala	66.66% <ø> (ø)
...syte/apalache/tla/bmcmt/rules/aux/CherryPick.scala	93.62% <100.00%> (+0.01%)	⬆️
...a/at/forsyte/apalache/tla/lir/TlaLevelFinder.scala	95.83% <0.00%> (+2.08%)	⬆️

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

[konnov]

Amazing fix. It's interesting to see how an optimization introduced non-deterministic behavior :)