solidity/test/libsolidity/smtCheckerTests/invariants/loop_array.sol
2019-09-13 12:40:53 +02:00

20 lines
367 B
Solidity

pragma experimental SMTChecker;
contract Simple {
uint[] a;
function f(uint n) public {
uint i;
while (i < n)
{
a[i] = i;
++i;
}
require(n > 1);
// Assertion is safe but current solver version cannot solve it.
// Keep test for next solver release.
assert(a[n-1] > a[n-2]);
}
}
// ----
// Warning: (273-296): Assertion violation happens here