I've been looking at various SMT solvers, mainly Z3, CVC4, and VeriT. They all have vague descriptions of their ability to solve SMT problems with quantifiers. Their documentation is primarily example based (Z3), or consists of academic papers, describing possible changes that may or may not actually be implemented.
I know that there are decidable fragments of First-order logic, such as:
What I'd like to know is, which (if any) classes of FOL are the various SMT solvers guaranteed to be complete for? How can I know whether a problem I'm looking at is in the fragments they are complete for?
There are two categories of quantified formulas that CVC4 is complete for.
(1) Quantified formulas with finite domains.
CVC4 is finite-model-complete on quantifiers over uninterpreted sorts, meaning that if there is a model where all uninterpreted sorts are interpreted as finite, then CVC4 will eventually find it. For details, you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
which summarizes the conference papers here:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Notice that these techniques combine with any theory supported by CVC4. Provided that the theory is decidable and the quantification does not involve (infinite) interpreted sorts, then the finite-model-completeness guarantee remains.
The approach is also refutation-complete for certain fragments, such as the Bernays-Schoenfinkel-Ramsey fragment (EPR), meaning that for any unsatisfiable problem in this fragment, CVC4 will eventually answer "unsat".
If you are interested in this feature, CVC4 will not by default use finite model finding on an input problem. The command-line option "--finite-model-find" will enable these techniques.
(2) Quantified formulas in some theories that emit quantifier elimination.
For example, CVC4 is complete for (pure) quantified linear arithmetic. For details you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
which builds upon an earlier conference paper:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf
This is similar in spirit to other approaches, for instance in Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf