solidity/test/libsolidity/smtCheckerTests/functions/getters/contract.sol

16 lines
390 B
Solidity

contract D {}
contract C {
D public d;
function f() public view {
D e = this.d();
assert(address(e) == address(d)); // should hold
assert(address(e) == address(this)); // should fail
}
}
// ====
// SMTEngine: all
// ----
// Warning 6328: (141-176): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.f()