[SMTChecker] Add test that has an unused mapping

This commit is contained in:
Leonardo Alt 2020-05-23 21:51:59 +02:00
parent 7a6ad61583
commit 0fda5fe077

View File

@ -0,0 +1,17 @@
pragma experimental SMTChecker;
contract C {
uint x;
uint y;
mapping (address => bool) public never_used;
function inc() public {
require(x < 10);
require(y < 10);
if(x == 0) x = 0; // noop state var read
x++;
y++;
assert(y == x);
}
}