solidity/test/libsolidity/smtCheckerTests/loops/while_2.sol
2019-12-09 15:32:08 +01:00

16 lines
201 B
Solidity

pragma experimental SMTChecker;
contract C {
function f(uint x) public pure {
x = 2;
while (x > 1) {
if (x > 10)
x = 2;
else
--x;
}
assert(x < 2);
}
}
// ====
// SMTSolvers: z3