[SMTChecker] Contract invariants - support nested quantifiers

From https://github.com/ethereum/solidity/pull/11451
We already report most contract invariants, but some of them (example: `crypto_functions_same_input_over_state_same_output.sol`) have nested quantifiers. Since bound variables only have an index and are defined by quantifier scope, they need a bit more care when being translated into `smtutil::Expression`. As a first step we left that out of that first PR, and it should be done in a different one.

Start with the referenced PR 11451 and the example contract invariant in crypto_functions_same_input_over_state_same_output.sol. Trace how bound variables are translated into smtutil::Expression, then verify that nested quantifier scopes are handled and the contract invariant is reported correctly.

Written by the indexing model from the issue text.