SSA conversion crash caused by extern array declaration

[andreast271]

CBMC version: 5.79.0
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: Verification failed
What happened instead: invariant violation report, abort, core dumped

An example C file that shows the problem is attached:
main.c.txt

The error message is:

Passing problem to propositional reduction
converting SSA
--- begin invariant violation report ---
Invariant check failed
File: arith_tools.cpp:173 function: from_integer
Condition: false
Reason: Precondition

The reason for the crash is that flattening tries to unpack an array where the array size is nil.

[tautschnig]

Thank you very much for your carefully crafted test case and the debugging already done. We are working on a fix, just need to decide whether to address this in the C front-end or the flattening code.