Fix prover upgrade policy 'remove'
The commit 5fc911ca adds a new policy called 'remove' for prover upgrades. This commit has several flaws
- exception BadID may appear in the IDE, which makes the interface in bad state
- the replay command may not terminate anymore (e.g. examples/test-provers/bv) see line 1016 in commit ebe5592a that may explain this
- It is not documented: please update section 4.2.2 of the manual
- What is it supposed to do anyway? If this should effectively remove proof attempt nodes from the session, then it should be implemented properly: in particular there is no point in adding a message like "prover removed" in the IDE, since the node in question is supposed to not be there anymore. Removing a node while still trying to make something appearing in the IDE may explain the BadID exceptions showing up
The commit ebe5592a is a temporary workaround for these bugs, allowing the replay to terminate