The SMT-COMP competition is held every year. https://smt-comp.github.io/2020/results.html https://smt-comp.github.io/2020/results.html Look up your problem dom

The SMT-COMP competition is held every year. https://smt-comp.github.io/2020/results.html https://smt-comp.github.io/2020/results.html Look up your problem domain and see how they compare. A nice thing about the smtlib2 format is that you can try the same problem in different solvers without too much pain. Generally every solver will out perform other solvers on at least some problems. For general purpose use, Z3 is a good starting point. I've had good luck with Boolector. I haven't really tried dreal. It is specialized for problems involving nonlinear predicates over real numbers, so it targets a different application domain than the other solvers.