[SMTChecker] Adding test witnessing that SMTChecker no longer crashes when producing CEX with arrays

This commit is contained in:
Martin Blicha 2020-12-09 09:13:39 +01:00
parent 0d7f9ae183
commit de34fe8aa3

View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(bytes calldata x, uint y) external pure {
x[8][0];
x[8][5*y];
}
}
// ----
// Warning 4984: (118-121): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.