solidity/test/libsolidity/smtCheckerTests/loops/while_bmc_iterations_8.sol

19 lines
272 B
Solidity

contract C
{
uint256[] y;
function f() public view {
uint256 x = 0;
while (x < y.length) {
x = 1;
}
// tests that constant condition warning is not reported
require(x != 0);
}
}
// ====
// SMTEngine: bmc
// SMTSolvers: z3
// BMCLoopIterations: 1
// ----