Arne Keller

You will need to update `taclets.old.txt` as described in `TestTacletEquality.java`.

> What does "changing the global font factor" mean exactly? Is that a setting within the operating system or a Java setting or done within the application? It refers to...

I have identified and fixed another issue where origin tracking could not be fully disabled (PR following shortly).

This is the hash code used for the map: https://github.com/KeYProject/key/blob/cacc0fbdfd54c51321ac4fd9dac8c246ebbc6ad2/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java#L735-L739 I think performance can be improved by adding more data to the hash code. For example the term depth must...

> I replaced it with the hashing function in [gist.github.com/mattulbrich/28c0f53f5a9f608c8c86f2ab1da39546](https://gist.github.com/mattulbrich/28c0f53f5a9f608c8c86f2ab1da39546), and it produced proofs of almost the same runtime (and same number of rule apps). I do think it has...

> Ok, that obviously depends on the program to load. I apparently looked at a smaler program. Which example do you use for reference? I use https://gist.github.com/FliegendeWurst/9be15e20e3bfd0722fcdd7f5c4afebcd. It requires some...

With some more optimizations it is possible to eliminate this particular slowdown:  Now the other bit of logic in the Simplifier takes approx. 90% of the CPU time. This...

> Regarding selectOfStore etc. Christoph Scheben implemented a set of taclets which pull out common heap terms such that such select-store chains need not be reduced more than once. It...

I have done some more tests on [ShortestPath.java](https://gist.github.com/FliegendeWurst/9be15e20e3bfd0722fcdd7f5c4afebcd): | Settings | Proof | Rule apps | Time | :---------:|:-----:|:---------:|:-----: `No origin tracking, OSS: with additional rules` | 3008 nodes |...

I think it may be necessary to use something like https://github.com/google/re2j instead of plain Java Regex