handling of smoke detection in sessions
SPARK now has a switch --proof-warnings that enables a number of extra checks via VCs that are of the "smoke detection" type, that is, if they are proved, something is wrong (and a warning is issued to the user). I believe why3 testing also uses some kind of smoke detection.
In most cases, no smoke is detected, so the VCs remain unproved. However, the unproved goal is still stored in the session. This is not very nice when the user looks into the session, which is now polluted with lots of unproved goals, even though all "real" VCs might be proved. The user can directly see the session via why3ide, or the manual proof feature of SPARK, or even by looking at the session file (a common way of looking at the session file would be via the "diff" feature of the version control system, if the session file is checked in).
It is unclear to me how this situation should best be improved. For example, the various tools (why3ide, SPARK manual proof) could hide by default smoke detection goals. That would require such goals to be marked specially (via an attribute?). Does the Why3 team have an idea how to deal with this, given that you already have a lot of experience with smoke detection?