Incorrect SSA for conditional state variable mutation

Slither gives incorrect SSA for the following program involving a state variable:
```solidity
contract State {
int state = 0;
function f(int a) public returns (int) {
if (a < 1) {
state += 1;
}
return state;
}
}
```

Here is the resulting SSA:
```
f:
state_1(int256) := ϕ(['state_0', 'state_2'])
TMP_0(bool) = a_1 < 1
CONDITION TMP_0
state_2(int256) = state_1 + 1
RETURN state_2
```

The return instruction relies on state_2 which is only conditionally defined. If `a_1 < 1` evaluates to false I would say this SSA form crashes (or the logical equivalent). An alternative SSA might look like:

```
f:
state_1(int256) := ϕ(['state_0', 'state_2'])
TMP_0(bool) = a_1 < 1
CONDITION TMP_0
state_2(int256) = state_1 + 1
state_3 = ϕ(['state_1', 'state_2'])
RETURN state_2
```