solidity/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol
2021-04-08 21:03:39 +02:00

14 lines
179 B
Solidity

contract Simple {
function f(uint x) public pure {
uint y;
require(x > 0);
while (y < x)
++y;
assert(y == x);
}
}
// ====
// SMTEngine: all
// SMTSolvers: z3
// ----