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

## 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

```solidity
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.