Termination plugin can cause verification progress to exceed 100% about viperserver HOT 3 CLOSED

over.vpr.txt
Here is a good example. Verification of the method does not terminate, so we can see the result of verifying the function. Proving termination on the function involves generating three additional methods. After they (and the function) have been verified, we end up at 4 results / 2 members => 200% verification.

from viperserver.

At first glance, it feels like the 'clean' solution to this would be to try to get the termination plugin to transform these multiple verification results back into one so that ViperServer only ever receives a single result for each member of the original parsed AST.

Edit: This is hard in the current plugin system. While we can do transformations on EntityResults, they always have to return a new result, so joining results together is difficult.

from viperserver.

New idea: emit a second StatisticsReport (maybe also adding a phase field to avoid confusion). This allows updating the ProgressCoordinator with the actual number of members to be verified.

from viperserver.