static initializer of a flexible array member is silently dropped

[71iq]

Version

CBMC version: 6.10.0 (cbmc-6.10.0-29-g357954eca6, develop)
Operating system: Linux x86_64

Code to reporoduce

#include <assert.h>
struct s {long a; int b; int tab[]; }; /* tab: flexible array member (FAM) */
struct s val = {0, 0, {42, 1337}}; /* static FAM initializer (GCC extension) */
int main()
{
  assert(val.tab[0] != 42); /* tab[0] is 42, so this MUST fail */
  return 0;
}

Behavior

I expect the assertion to fail, or if static FAM initialization is considered out of scope, CBMC should reject/error on it rahter than silently reading wrong values.

What happened instead was:

[main.assertion.1] line 6 assertion val.tab[0] != 42: SUCCESS
VERIFICATION SUCCESSFUL