[mmoskal]

It is indeed magical with largely unpredictable run times, especially once you venture into undecidable fragments (quantified formulas). There is a million heuristics that you can tune (and indeed there have been attempts of using ML for that; ML is mostly useless for the actual reasoning). Using quantifiers with SMT is a bit like programming in Prolog though much more non-deterministic.

However, for the simpler (just NP-complete) problems the run times are more predictable. If your problem has a streight-forward encoding into SMT, you should definitely try it. The common format also makes it relatively easy to swap tools like CVC and Z3.

[freemint]

Quantified SAT is decidable. Are you aware of any theories where expressions with quantors over finitely many choices are unsatisfiable but quantor free expressions are satisfiable over the same theory?