[SMTChecker] CHC report loop invariants

[leonardoalt]

Depends on https://github.com/ethereum/solidity/issues/14325

Currently we support exporting contract and reentrancy invariants to the user. We should also export loop invariants. This means that in Invariants.cpp we need to add loop_header (or whatever the prefix used for loop header predicates is in CHC.cpp) to the search targets.

[hrkrshnn]

What kind of invariants? Can it detect that a memory struct declared inside is invariant?

[leonardoalt]

If you write a property that represents that, it could. But what I mean is:

y = 0;
while (y < x)
  ++x;
assert(x == y);

y <= x is an inductive invariant for the loop, that is, it is true every time the condition is checked. The assertion is proved by "replacing" the loop by its inductive invariant and adding the negated condition as a constraint after the loop: y <= x && y >= x => y == x

[leonardoalt]

Let's wait with this one until we refactor the solvers to use only the smtlib2 interface: https://github.com/ethereum/solidity/issues/14325