[SMTChecker] Buggy invariants

[leonardoalt]

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);
    }
}

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

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

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

[leonardoalt]

This requires some investigation on what's coming back from the solver (I assume this bug is on our side), and why we're translating it to true.

[leonardoalt]

Turns out this is more complicated than we initially thought. z3 sends invariants as disjunctions which breaks some assumptions we had. The main problem is that the disjunctions have some complicated operands with nested quantifiers which are hard to encode.

We're not sure yet how to solve this.