-
See http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/ We use a "runLen" array of size 128, so it should be nearly impossible to have our implementation overflow. But in any case, the fix is relatively simple -- checking two extra conditions in the invariant calculation. I also took this opportunity to remove some redundancy in the left/right merge logic in the invariant loop.
9b987f8c