CBMC missing an error after exiting do-while loop

[mksvoboda97]

Description

For some reason, CBMC does not report the assertion violation for the program below:

#include <stdlib.h>
#include <assert.h>
typedef struct node
{
  int data;
}
 *SLL;
int main ()
{
  const int len = 0;
  SLL last = malloc (sizeof (struct node));
  if (NULL == last) exit(0);
  last->data = 0;
  SLL ptr = last;
  do
    {
      if (ptr->data)
        {
          goto ERROR;
        }
      ptr->data = 1;
    }
  while (ptr != last);
  len;
ERROR: assert(0);
}

While the GOTO statement is unreachable, the assertion should still be reached once the program exits the loop, i.e. after the first iteration.
Notably, the assertion is found when I drop the unrelated len; statement (which should have no effect).

Version:

Latest (built from fd5dcee);
Full version string: CBMC version 6.11.0 (cbmc-6.11.0-6-gfd5dcee9e6) 64-bit x86_64 linux

Full output:

$ cbmc test.c
CBMC version 6.11.0 (cbmc-6.11.0-6-gfd5dcee9e6) 64-bit x86_64 linux
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is UNSATISFIABLE

** Results:
<builtin-library-malloc> function malloc
[malloc.assertion.1] line 31 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 36 max allocation may fail: SUCCESS

test.c function main
[main.pointer_dereference.1] line 13 dereference failure: pointer NULL in last->data: SUCCESS
[main.pointer_dereference.2] line 13 dereference failure: pointer invalid in last->data: SUCCESS
[main.pointer_dereference.3] line 13 dereference failure: deallocated dynamic object in last->data: SUCCESS
[main.pointer_dereference.4] line 13 dereference failure: dead object in last->data: SUCCESS
[main.pointer_dereference.5] line 13 dereference failure: pointer outside object bounds in last->data: SUCCESS
[main.pointer_dereference.6] line 13 dereference failure: invalid integer address in last->data: SUCCESS
[main.pointer_dereference.7] line 17 dereference failure: pointer NULL in ptr->data: SUCCESS
[main.pointer_dereference.8] line 17 dereference failure: pointer invalid in ptr->data: SUCCESS
[main.pointer_dereference.9] line 17 dereference failure: deallocated dynamic object in ptr->data: SUCCESS
[main.pointer_dereference.10] line 17 dereference failure: dead object in ptr->data: SUCCESS
[main.pointer_dereference.11] line 17 dereference failure: pointer outside object bounds in ptr->data: SUCCESS
[main.pointer_dereference.12] line 17 dereference failure: invalid integer address in ptr->data: SUCCESS
[main.assertion.1] line 25 assertion 0: SUCCESS

** 0 of 15 failed (1 iterations)
VERIFICATION SUCCESSFUL