E-matching is the most commonly used technique to handle quantifiers
  in SMT solvers. It works by identifying characteristic
  sub-expressions of quantified formulae, named triggers, which are
  matched during proof search on ground terms to discover relevant
  instantiations of the quantified formula. E-matching has proven to
  be an efficient and practical approach to handle quantifiers, in
  particular because triggers can be provided by the user to guide
  proof search; however, as it is heuristic in nature, e-matching
  alone is typically insufficient to establish a complete proof
  procedure. In contrast, free variable methods in tableau-like
  calculi are more robust and give rise to complete procedures, e.g.,
  for first-order logic, but are not comparable to e-matching in terms
  of scalability. This paper discusses how e-matching can be combined
  with free variable approaches, leading to calculi that enjoy similar
  completeness properties as pure free variable procedures, but in
  which it is still possible for a user to provide domain-specific
  triggers to improve performance.