Linking errors when compiling static smt-switch with multiple SMT solvers that share dependencies

[CyanoKobalamyne]

Compiling smt-switch with --static and both Boolector and Cvc5 results in numerous linking errors of the form:

multiple definition of `CaDiCaL::Solver::XXXXXXXXX'

Where XXXXXXXXX can be a number of things.

This is because both solvers use Cadical under the hood (at least in our configuration) and we "repack" static libraries to include all dependencies. I'm assuming this is a well-intentioned feature that is supposed to allow users to just link against libsmt-switch.a and libsmt-switch-solver.a for the solver that they want to use. However, this breaks a whole host of assumptions that the Linux/Unix tooling ecosystem makes about how static libraries work and results in the errors above.

I think that there are two possible solutions to this:

1. We do what every other "normal" Linux/Unix static library does: produce static library archives that only contain our own object files, as well as some information (e.g. as a pkg-config .pc file or a CMake config file, or both) about how they ought to be linked against.
2. We preserve the current behavior where users don't need to include direct and transitive solver dependencies among the linking flags but produce a single, merged static library file that has exactly one copy of each dependency, even when multiple dependencies have the same transitive dependency, like in this case. This, however, puts a significant maintenance burden on us as we need to manage the dependencies' dependencies all on our own and need to find versions that work with each other.