Arne Keller
Arne Keller
## Intended Change This PR fixes a slicing failure with a specific proof. In that particular case, the dynamically added taclet was slightly too different for the previous code to...
This PR expands the proof caching infrastructure by introducing an external database of proofs. Proofs are currently added manually by the user to the database. The user may inspect the...
Experiment to logically group steps in proof. Two main features: - "Reorder" proof steps such that adjacent proof steps modify the same formula (no interweaving of two simplification chains) -...
## Description Try to load the file below. It contains a syntax error (`==` instead of `=` in the problem statement), but the error message produced by KeY is bad:...
## Description `sort_Field` is not defined, but used here: https://github.com/KeYProject/key/blob/022f0facc33017f34bba2df8594a5fb40678d3cc/key.core/src/main/resources/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.preamble.xml#L14 ## Reproducible always ### Steps to reproduce 1. Load some proof (I used Exercise7.java from #1000) 2. Do some simplifications...
This PR is an alternative to #3272, it only includes the optimizations. See the commits in this branch for details. Short description of each optimization: - replaceKnown is called only...
## Description The keyboard shortcut for the auto mode (ctrl + space) cannot be used when the proof tree or the task tree is focused. ### Steps to reproduce 1....
This PR adds a new option to the proof tree to "linearize symbolic execution". This option changes the proof tree to be slightly more linear. In effect, the "Normal Execution"...
## Description See title ## Reproducible always ### Steps to reproduce 1. Load a proof with filename e.g. `x_sliced.proof` 2. Try to slice it Expected: works Actual: doesn't ### Additional...
## Description When trying to run e.g. Finish Symbolic Execution nothing happens. Running the macro again then works as expected. Perhaps related: sometimes the OSS is only used after some...