[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.