CBMC error if variable of type struct with flexible array member is forward declared and initialized

[andreast271]

CBMC version: cbmc-5.54.0-13-gf3e4096300
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc fam.c
What behaviour did you expect: termination with message VERIFICATION SUCCESSFUL and exit status 0
What happened instead: termination with message CONVERSION ERROR and exit status 6

The error occurs in the following scenario:

1. There is a struct St with a flexible array member
2. A global variable with type St is both forward declared and initialized

The test case fam.c.txt is attached.
The output is in file cbmc.log.

The problem was introduced by the following commit:
commit b16c7d7
Author: Michael Tautschnig tautschn@amazon.com
Date: Fri Feb 11 13:17:17 2022 +0000

Reverting commit b16c7d7 on top of commit f3e4096 fixes the error, but I did not check if it causes other problems.

[tautschnig]

Thank you for the detailed report and the test case! #6788 now fixes the problem (without having to revert b16c7d7).