[SMTChecker] Bug: Inconsistent Storage Array Bytes Writing about solidity

[blishko]

Hi @sallywang147,

do I read it correctly that you are using solc 0.7.0? That is rather old version of the compiler, SMTChecker has matured significantly since then.

On the latest version, I see different results from SMTChecker.
Can you check with the latest version and let us know if you still consider the answers incorrect?

One note about your examples:

uint128[] memory y;// = new uint128[](1);
y[0] = 23;

This is an access out of bounds, so the code would always revert at this point, making the assertions that follow always unreachable (and thus safe).

[sallywang147]

Hi @blishko, many thanks for your quick response! I totally agree that the newer compiler version (>=0.8.0) would prevent this issue. On 0.7.0, I think the root cause is not SMTChecker but the older compiler. For example, the 0.7.0 compiler generated x[0] = 0 when it really should've been x[0] = 23. That's why SMTChecker throws the violation when it executes the assertion assert(x[0]==23);. Is this explanation plausible? or in your view, is the issue caused by something else? Many thanks for your time!

[blishko]

I suspect that the SMTChecker warnings are independent of the code generated by the compiler.
Unfortunately, we cannot afford to investigate the behaviour in the old version of the compiler when the new version does not suffer from this issue.

[sallywang147]

Ah no worries at all, many thanks again for your quick response! I'll close the comment.