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

[blishko]

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.

Tasks

Preview Give feedback

1. Add support for parsing SMT-LIB
2. Add support for invariants from Eldarica
3. SMTChecker: Add support for counterexamples from Eldarica #15706
   smt +1
4. Support Z3 through SMT-LIB interface
5. Switch completely to SMT-LIB interface and drop solvers' libraries

[blishko]

Everything except counterexamples from Eldarica have been done and the solvers are now used through SMT-LIB interface.
The switch for Z3 was done here: #15252