solidity/test/libsolidity/smtCheckerTests/inheritance/implicit_constructor_hierarchy.sol

20 lines
329 B
Solidity
Raw Normal View History

contract A {
uint x;
2020-06-23 12:14:24 +00:00
constructor (uint y) { assert(x == 0); x = y; }
}
contract B is A {
2020-06-23 12:14:24 +00:00
constructor () A(2) { assert(x == 2); }
}
contract C is B {
function f() public view {
assert(x == 2);
}
}
// ====
2021-03-31 15:11:54 +00:00
// SMTEngine: all
// SMTSolvers: z3
// ----
2021-10-06 09:53:03 +00:00
// Info 1180: Contract invariant(s) for :C:\n(!(x <= 1) && !(x >= 3))\n