[SMTChecker] Buggy invariants

```solidity
contract S {
uint x;

function setZero() external {
if (x == 1)
x = 0;
}

function setOne() external {
if (x == 0)
x = 1;
}

function inv() external view {
assert(x < 2);
}
}
```

```bash
solc s.sol --model-checker-engine chc --model-checker-invariants contract`
```

The command above gives the invariant below which is clearly wrong.

```bash
Info: Contract invariant(s) for s.sol:S:
(true || true || !(x >= 2) || true)
```

Reproduce the issue with solc s.sol --model-checker-engine chc --model-checker-invariants contract using the Solidity contract shown. Start by tracing SMTChecker's contract-invariant generation and compare the reported invariant with the assert in inv(). Done means the generated invariant no longer contains the incorrect tautological clauses and reflects the contract's actual invariant.

Written by the indexing model from the issue text.