Inconsistent postconditions

[hajduakos]

trafficstars

While #57 was fixed by havocing the variables, the developer can still introduce inconsistencies (e.g. by mistake) with the postconditions of unimplemented/skipped functions:

contract C {
    int x;

    function f() public {
        x = 1;
        g();
        assert(false);
    }

    /// @notice modifies x
    /// @notice postcondition x == 0
    /// @notice postcondition x == __verifier_old_int(x)
    function g() public;
}

The code above will not report any error due to the postconditions being assumed and being inconsistent with x = 1 before the function. If there was some "real" code instead of assert(false) the developer would falsely think that it is correct.