solidity/test/cmdlineTests/model_checker_bmc_loop_iterations/input.sol

12 lines
181 B
Solidity
Raw Permalink Normal View History

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract C
{
function f(uint x) public pure {
require(x == 0);
do {
++x;
} while (x < 2);
assert(x == 3);
}
}