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

16 lines
187 B
Solidity

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