Better path error reporting #5628
Description
Dafny currently may, when postconditions can not be proven, report a specific return location where those could not be proven, in case there are different return locations. However, this does not always work reliably, like here, where we would hope the error is shown in the then branch of the if:
In other cases, the error only occurs for a specific path, but for all return locations, like here:
So Dafny will not indicate a useful path location by design.
A better UX might be that if only particular branches lead to the exception, that Dafny would tag these branches as related locations.