Information Flow proofs are not re-loadable

[wadoon]

Description

Due to an internal Taclet generation, Information Flow proofs are not reloadable. The generation uses makeUnique, which uses a global static register to check for name collision. Naming collisions are resolved by incrementing a counter (alreadyRegistered).

This counter destroys the deterministic behavior of proofs and their reloadability.

Reproducible

Is the issue reproducible?

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

1. Start KeY.
2. Load an Infflow example that requires a dependency contract.
3. Auto play
4. Store proof.
5. Load proof w/o restarting KeY.
6. Loading fails as the Taclet name now differ.

What is your expected behavior and what was the actual behavior?

KeY should load successfully.

Additional information

Add more details here. In particular: if you have a stacktrace, put it here.

---

• Commit: main / Release 2.13.0