[SMTChecker] Improve usability

The SMTChecker's usability is still not great, especially for new users.
When running the SMTChecker on large contracts with the default settings, users are often bombarded with warnings about targets the solver couldn't prove, and verifying all contracts at the same time makes the encoding very large.
A few items that could be improved:

- [x] There is a lot of noise about targets that the solver could not prove. One idea is to compress all of those into a single warning by default, saying `128 verification conditions could not be proved. Consider choosing a single contract to be verified. To see the full list of unproved targets, enable model checker verbosity to 2` for example. This would also highlight problems that are actually confirmed.
- [x] Underflow/overflow verification conditions create A LOT of targets which really bloats the solver. IMO, these should not be checked by default for Solidity >=0.8.0 since most people do rely on the compiler's built-in checks. Conclusion, I think we should not check for underflow/overflow by default for Solidity >=0.8.0.
- [ ] Choosing a single contract to be verified increases performance a lot. Somehow deciding on a single contract (or a few) by default could also improve usability a lot.
- [x] Filter unsupported warnings by target contract reachability https://github.com/ethereum/solidity/issues/11703

The only unchecked item is choosing one or a few contracts by default for SMTChecker verification to improve usability and performance. No files or tests are named, so first locate the SMTChecker verification and contract-selection entry points, then define and test the default-selection behavior; done means large runs avoid verifying every contract by default while preserving explicit selection.

Written by the indexing model from the issue text.