Skip to content

Commit ee3e2b7

Browse files
committed
Undo determinism fix of previous commit for backwards compatibility
1 parent 118a542 commit ee3e2b7

1 file changed

Lines changed: 1 addition & 9 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -207,15 +207,7 @@ private void initIndices(Proof proof) {
207207
ImmutableList<String> done = ImmutableList.nil();
208208
for (String ruleSet : ruleSets) {
209209
ImmutableList<Taclet> taclets = tacletsForRuleSet(proof, ruleSet, done);
210-
// Sort by name for a deterministic index: the taclets are collected in set
211-
// iteration order, and when several rules match at the same position the
212-
// simplifier applies the first one found. Without a canonical order, the
213-
// aggregated simplification result may differ between proof instances of the
214-
// same problem (e.g. between a proof and its replayed or elaborated copy).
215-
final ArrayList<Taclet> sorted = new ArrayList<>();
216-
taclets.forEach(sorted::add);
217-
sorted.sort(Comparator.comparing(t -> t.name().toString()));
218-
indices[i] = TacletIndexKit.getKit().createTacletIndex(sorted);
210+
indices[i] = TacletIndexKit.getKit().createTacletIndex(taclets);
219211
notSimplifiableCaches[i] = new LRUCache<>(DEFAULT_CACHE_SIZE);
220212
i++;
221213
done = done.prepend(ruleSet);

0 commit comments

Comments
 (0)