Extern array declaration causes unsupported array typecast in smt2 conversion

[andreast271]

CBMC version: CBMC version 5.12 (cbmc-5.12.2-3-g9b5f761d5-dirty)
Operating system: 64-bit x86_64 linux
Exact command line resulting in the issue: cbmc --smt2 def.c use.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead: invariant violation

Example:
backtrace.log
def.c.txt
use.c.txt

Explanation of the example:
file def.c defines an array of fixed positive size. file use.c contains an extern declaration for this array and uses it. When the array is accessed with a non-constant index, this is translated in the program equation to a byte extract expression

byte_extract(base, offset)

where base is a typecast of the array defined in def.c to an array with size nil. This typecast from int[3] to int[] is not supported in smt2 conversion. It's not clear to me if the typecast is even necessary here. Shouldn't the array in file use.c and the array in file def.c be the same object, the type of which is int[3]?

[martin-cs]

This looks like a bug. There have been some recent patches to the SMT-LIB 2 back-end which may have broken things. I think this should work, would you be able to try an earlier version and see if this is a regression?

[andreast271]

I ran the example with versions 5.12 and 5.11 and got the same invariant violation as with the latest version from the develop branch.

[martin-cs]

Thanks for checking that out.

[tautschnig]

This was fixed in 914f3d6 (#6188), which is included in 5.37.0 and any later release.