[SMTChecker] CHC report loop invariants

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.

Start by reviewing the dependency in issue #14325, then inspect Invariants.cpp and the loop-header predicate naming in CHC.cpp. Confirm how contract and reentrancy invariants are selected, add loop invariants to the same export targets, and verify that loop invariants are reported to users.

Written by the indexing model from the issue text.