solidity/test/libsolidity/smtCheckerTests/bmc_coverage/math_constructor.sol
2022-04-01 23:41:18 -05:00

9 lines
172 B
Solidity

contract C {
uint z = 1;
uint w = z - 3;
}
// ====
// SMTEngine: bmc
// ----
// Warning 4144: (36-41='z - 3'): BMC: Underflow (resulting value less than 0) happens here.