byte_extract is not appearing on the rhs of trace assignment when using the incremental smt2 decision procedure

[esteffin]

When generating a trace using the incremental smt2 decision procedure, if an assignment of the form byte_extract(x, y, z) = byte_extract(j, k, l) should be present, it will be shown as byte_extract(x, y, z) = some_other_printout.

This causes a failure of test:

• cbmc/trace-values/unbounded_array.desc

as it expects to find the trace step:
byte_extract_little_endian(dynamic_object, 0l, signed int [2l])=byte_extract_little_endian({ [0ul]=1, [1ul]=2, [13ul]=42 }, 0l, signed int [2l]) (?)

but it instead finds:
byte_extract_little_endian(dynamic_object, 0l, signed int [2l])={ 1, 2 } ({ 00000000 00000000 00000000 00000001, 00000000 00000000 00000000 00000010 })

[tautschnig]

This RHS just looks like the simplified version of what the test expects? Maybe that's actually ok and we should change the test instead?