contract A { int x = 0; function f() virtual internal view { assert(x == 0); } function proxy() public view { f(); } } contract C is A { function f() internal view override { assert(x == 1); } } // ==== // SMTEngine: all // ---- // Warning 6328: (227-241): CHC: Assertion violation happens here. // Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.