[OxO4]

> SAT solving is about 95+% of SMT solving

This is theory-dependent, I would say. It is certainly true for bit-vector solvers that bit-blast for example. For other theories, however, this is not necessarily the case. Consider a simplex-based linear integer arithmetic solver for example. If there is a problem that is simple at the Boolean level, you may end up spending more time in the simplex solver.

[zero_k]

Ah, good point. Still, the most used theories are mostly SAT-bound. BV (bitvector) especially. And the translation to SAT can play a huge part, so even in BV logics, the SMT solver's abilities are super-important. But runtime in these logics are dominated by the SAT solver. I should play with more SMT solvers.

I work on the STP SMT solver along with a team of very dedicated people (https://github.com/stp/stp/), it's QF_BV (Quantifier Free BV) solver and it tends to do well in the competitions: https://smt-comp.github.io/2020/results.html So I'm probably a bit biased towards BV. For counting (e.g. https://github.com/meelgroup/approxmc) and sampling (e.g. https://github.com/meelgroup/unigen) it's also 99% SAT solver runtime.