CBMC crashing with byte_extract flatting with non-constant size: byte_extract_little_endian

[thk123]

When running with a sufficently large --depth argument, CBMC can produce the following error:
byte_extract flatting with non-constant size: byte_extract_little_endian

Full log: json_decode_error.txt

Source file: https://github.com/jpmens/jo/blob/2bedfd486f8f4a79b1865e370e6c858eb04257f5/json.c

Command line: cbmc json.c --function json_decode --depth 150 --cover location

[tautschnig]

This has been fixed in #795 (237d8be).