solidity/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol
2023-02-06 17:02:33 +01:00

22 lines
387 B
Solidity

contract D {
uint x;
function s(uint _x) public { x = _x; }
function f() public view returns (uint) { return x; }
}
contract C {
D d;
constructor() {
d = new D();
}
function g() public view {
assert(d.f() == 0); // should fail
}
}
// ====
// SMTContract: C
// SMTEngine: all
// SMTExtCalls: trusted
// ----
// Warning 6328: (204-222): CHC: Assertion violation happens here.