[SMTChecker] Unreachable code inside a loop with if statement and break statement in its body is not detected

[pgebal]

Environment

• Compiler version: commit https://github.com/ethereum/solidity/commit/a1b79de64235f13e6b06e088fe6365c5a12d13d3

Steps to Reproduce

Use the following standard json settings file:

{
    "language": "Solidity",
    "sources": {
        "C.sol": {
            "urls": ["./C.sol"]
        }
    },
    "settings": {
        "modelChecker": {
            "contracts": {
                "C.sol": ["C"]
            },
            "engine": "bmc",
            "showUnproved": true,
            "solvers": ["z3"],
            "targets": ["assert"]
        }
    }
}

to compile the following contract

contract C {
        function f() public pure {
            uint x = 0;
            while (x < 3) {
                if (x >= 0) {
                    ++x;
                    break;
                }
                ++x;
            }
            assert(x == 1);
        }
    }

unreachable code in line 9 is not reported.

[pgebal]

I've given a bad example. It's not about any unreachable code. It's about when a conditation or an assert is used in unreachable code. Example:

contract C {
        function f() public pure {
            uint x = 0;
            while (x < 3) {
                if (x >= 0) {
                    ++x;
                    break;
                }
                if (x == 1)
                             x == 2;
            }
            assert(x == 1);
        }
    }

Then condition in line 9 should be reported as unreachable.