SMTChecker: Use SMT-LIB interface instead of solvers' APIs

This is an issue to keep track on the progress of replacing the usage of solvers' APIs with a unified way of using SMT-LIB interface.

My previous attempt to tackle this is in a PR draft #14369.
However, the task is too large to address in a single PR.
Thus we break it down to smaller steps:
We need to be able to parse responses of the solvers, which means we need to implement a parser for (a reasonable subset of) SMT-LIB format. Then we can support production of invariants and counterexample when using Eldarica.
Afterwards, we can add support for Z3 through SMT-LIB interface. If that works correctly, we can eventually remove Z3 as a library.

```[tasklist]
### Tasks
- [x] Add support for parsing SMT-LIB
- [x] Add support for invariants from Eldarica
- [ ] https://github.com/ethereum/solidity/issues/15706
- [x] Support Z3 through SMT-LIB interface
- [x] Switch completely to SMT-LIB interface and drop solvers' libraries
```