Coq can do everything Z3 does (with a few axioms mixed in)... except for the fast automation a SMT solver is all about :-). The decidable logic fragment Z3 was

Coq can do everything Z3 does (with a few axioms mixed in)... except for the fast automation a SMT solver is all about :-). The decidable logic fragment Z3 was king on for more than a decade — uninterpreted functions, linear arithmetic, arrays, bitvectors, and more recently datatypes, is quite restricted but for formulas that fit in it (possibly after encoding) Z3 will steamroll Coq's automation. That is, unless you use CoqHammer which just calls Z3 or cvc4 from Coq, of course.