fix replay of cleanup

KeYProject · Oct 27, 2023 · ea9009f · ea9009f
1 parent 6169ba5
commit ea9009f
Show file tree

Hide file tree

Showing 2 changed files with 7,976 additions and 735 deletions.
diff --git a/src/main/java/de/wiesler/Cleanup.java b/src/main/java/de/wiesler/Cleanup.java
@@ -315,7 +315,16 @@ public static void cleanup(
               @
               @ assignable values[start..stop - 1];
               @*/
-            {}
+            {
+                if (stop - start <= Constants.ACTUAL_BASE_CASE_SIZE || is_last_level) {
+                    //@ ghost \seq bucketValuesBeforeSort = \dl_seq_def_workaround(start, stop, values);
+                    // seqPerm(seq, seq2)
+                    // forall i in seq2; f(i) ==> forall i in seq; f(i)
+                    Sorter.fallback_sort(values, start, stop);
+                    //@ ghost \seq bucketValuesAfterSort = \dl_seq_def_workaround(start, stop, values);
+                    //@ assert (\forall int i; 0 <= i < bucketValuesAfterSort.length; classifier.classOf((int)bucketValuesAfterSort[i]) == bucket);
+                }
+            }
 
             /*@ assert \invariant_for(classifier) && \invariant_for(bucket_pointers) && \invariant_for(buffers) &&
               @     Functions.countElementSplit(values, begin, begin + \old(bucket_starts[bucket]), begin + \old(bucket_starts[bucket + 1])) &&