CBMC-cover tests fail due to an invariant violation

[reuk]

While working on #1612, I found an error in goto-instrument/cover.cpp. The problem is that the begin() of an empty vector is dereferenced, leading to undefined behavior.

Adding an invariant to ensure the vector has at least one element causes several tests in cbmc-cover to fail. These tests have been disabled in this commit.

The original author of the code appears to be @theyoucheng, so I suggest that they are assigned to fix this problem. The result of the fix should be that the failing tests are re-enabled.

[martin-cs]

Thanks @reuk for the informative summary.

@theyoucheng : please could you have a look at these, we really shouldn't have obvious code inputs which trigger invariant failures.

@peterschrammel might also be interested in this as he was refactoring some of the coverage code at one point.