Casts between different fixedbv types broken in goto-cc

[polgreen]

Casts between different sizes of __CPROVER_fixedbv seem to have broken at some point since release 5.7, when the analysis is performed on a binary produced by goto-cc. Here is a minimal example:

int main()
{
	__CPROVER_fixedbv[16][8] BV;
	__CPROVER_fixedbv[32][16] BV2;
	BV2 = 100;
	BV = (__CPROVER_fixedbv[16][8])BV2;

	__CPROVER_assert(0,"");

}

Commands used to compile with goto-cc and analyse

goto-cc test.c -o test.output
cbmc test.ouput

This produces the following error:

CBMC version 5.8 64-bit x86_64 linux
Reading GOTO program from file
Reading: output_develop.binary
failed to find __CPROVER_architecture_fixed_for_float

I'm using goto-cc and cbmc at commit d069719

When I follow the same steps with CBMC release 5.7 (and the version of goto-cc included with 5.7), the analysis runs fine.

When I run the analysis directly on the test.c file with either version of CBMC, it runs fine