Old expression casts to 256 bit

[hajduakos]

trafficstars

Currently we have two old(...) expressions, taking/returning int256 and int256 respectively, casting smaller integers to bigger ones. This might cause problems as demonstrated by the example:

pragma solidity>=0.5.0;

contract C {
    uint40 x;
    /// @notice postcondition x == __verifier_old_uint(x) + 1
    function f() public {
        x++;
    }
}

Running the example with --arithmetic mod solc-verify fails to prove the postcondition because x++ is calculated modulo 2^40 but __verifier_old_uint(x) + 1 is calculated modulo 2^256.

We could come up with __verifier_old_int_XXX(..) for each bit width but that does not seem so user friendly.