solidity/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol

22 lines
338 B
Solidity
Raw Normal View History

contract C {
uint[] b;
function f() public {
require(b.length == 0);
b.push() = 1;
assert(b[0] == 1);
}
function g() public {
b.push() = 1;
assert(b[b.length - 1] == 1);
// Fails
assert(b[b.length - 1] == 100);
}
}
2021-03-31 15:11:54 +00:00
// ====
// SMTEngine: all
// ----
2021-10-06 09:53:03 +00:00
// Warning 6328: (199-229): CHC: Assertion violation happens here.