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

17 lines
327 B
Solidity

contract A {
uint x = msg.value;
constructor() {
assert(x == 0); // should hold
}
}
contract B {
constructor() payable {
assert(msg.value == 0); // should fail
}
}
// ====
// SMTEngine: bmc
// ----
// Warning 4661: (154-176='assert(msg.value == 0)'): BMC: Assertion violation happens here.