Odd behavior when cleaning detached theories
Weird things seem to happen consistently when attempting to clean detached theories.
Synopsis:
- Prove the following file, save session, close IDE.
- Comment out theory B.
- Open IDE, theory B is detached.
- Focus the root node (the file), hit "clean".
The error message is "There was an unrecoverable error during treatment of request: command "clean" with exception: anomaly: Why3.Session_itp.BadID"
Following that, attempting to save the session gives a similar message, even when clicking "yes" in the prompt when trying to close the IDE, which means the user has to accept to quit the IDE without saving.
All is not lost though, because it appears that both the clean and the save were successful in the end (after closing/reopening the IDE one more time, theory B is gone and other changes seem to have been preserved).
module A
axiom A1: false
goal G: false
end
module B
axiom B1: false
goal H: false
end