SMT is often faster than explicit state exploration, especially in simple cases. OTOH, they sometimes don't work. AFAIK, the state-of-the-art (or of research) in fully automated verification is what's known as CEGAR model-checking, which uses SMT solvers to automatically reduce the state space, by finding automatic abstraction/refinement relations. The downside, AFAICT, of CEGAR, is that it requires some domain knowledge about the problem (although that domain knowledge may be provided by the user). There's a project under development called APALACHE (http://forsyte.at/research/apalache/), which is a CEGAR model-checker for TLA+, optimized for some distributed systems use-cases.
Ron