Conversions between fixed-size byte arrays of different lengths are wrong

[ellab123]

From Solidity v.0.6.1 doc:
If a fixed-size bytes type is explicitly converted to a larger type, it is padded on the right, for example:
bytes2 a = 0x1234;
bytes4 b = bytes4(a); // b will be 0x12340000

In VeriSol, the value of b is exactly the same as the value of a.

[shuvendu-lahiri]

the test is added as a comment in BytesTypes.sol by Ella.