No pointer check or bounds check failure and incorrect program equation for access of array in struct with negative index

[andreast271]

CBMC version: 6.4.1
OS: Linux x86_64

Test case:

#include <assert.h>
struct St {
  char a[2];
  char b[2];
};

int main() {
  struct St data = {{1,2},{3,4}};
  data.b[-1] = 5;
  assert(data.a[1] == 2);
  return 0;
}  

The index expression data.b[-1] is for most compilers equivalent to *(data.b - 1) == *(data.a + 1). I expected CBMC to either model this correctly, or produce a failing pointer check or array bounds check. However, neither is happening. The assertion is passing, so *(data.a + 1) is unchanged by the assignment preceding the assertion. Pointer check and bounds check do not produce an assertion, let alone a failing one.
The report by cbmc is the following:

$ cbmc neg_idx.c --pointer-check --bounds-check 
CBMC version 6.4.1 (cbmc-6.4.1) 64-bit x86_64 linux
Type-checking neg_idx
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking

** Results:
neg_idx.c function main
[main.assertion.1] line 11 assertion data.a[1] == 2: SUCCESS

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