CBMC does not detect reachable error label before return statement

[PhilippWendler]

When telling CBMC to look for error labels with the argument --error-label ERROR, it ignores labels that are directly before a return statement.

Example: cbmc --error-label ERROR returns "verification successful" for the following program:

int main() {
  goto ERROR;

  return 0;
  ERROR:
//  ;
  return 1;
}

If I add some other statement before the return (even by just removing the //), the result is "verification failed" as expected.

CBMC version: 5.36 (problem is present at least in 5.12 as well)
Operating system: the Docker container diffblue/cbmc:5.36.0
Exact command line resulting in the issue: cbmc --error-label ERROR program.c
What behaviour did you expect: Error label found as reachabled
What happened instead: Reachable error label ignored

[jimgrundy]

We are interested in coverage issues in general and we're concerned that perhaps this indicates a more general issue with coverage analysis.