[SMTChecker] Support delete

This commit is contained in:
Leonardo Alt
2019-05-06 18:32:10 +02:00
parent e99efec085
commit 2139c20776
8 changed files with 151 additions and 0 deletions
@@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract C
{
uint[] a;
function f(bool b) public {
a[2] = 3;
require(b);
if (b)
delete a;
else
delete a[2];
// Assertion fails as false positive because
// setZeroValue for arrays needs \forall i . a[i] = 0
// which is still unimplemented.
assert(a[2] == 0);
}
}
// ----
// Warning: (118-119): Condition is always true.
// Warning: (297-314): Assertion violation happens here