diff --git a/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol b/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol new file mode 100644 index 000000000..0d19b2877 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/delete_multid_array.sol @@ -0,0 +1,42 @@ +pragma experimental SMTChecker; + +contract C { + uint[] a; + uint[][] b; + function f(uint x, uint y, uint v) public { + a[x] = v; + delete a; + assert(a[y] == 0); + } + function g(uint x, uint y, uint v) public { + b[x][y] = v; + delete b; + assert(b[y][x] == 0); + } + function h(uint x, uint y, uint v) public { + b[x][y] = v; + delete b[x]; + // Not necessarily the case. + assert(b[y][x] == 0); + } + function i(uint x, uint y, uint v) public { + b[x][y] = v; + delete b[y]; + assert(b[y][x] == 0); + } + function j(uint x, uint y, uint z, uint v) public { + b[x][y] = v; + delete b[z]; + // Not necessarily the case. + assert(b[y][x] == 0); + } + function setA(uint x, uint y) public { + a[x] = y; + } + function setB(uint x, uint y, uint z) public { + b[x][y] = z; + } +} +// ---- +// Warning: (372-392): Assertion violation happens here +// Warning: (617-637): Assertion violation happens here