Quantifiers and SMT

used in verification as back-ends to check the satisfiability
of formulas in presence of interpreted symbols. After a brief
overview of their architecture, we will review the current
methods used in those solvers to handle quantifiers. An early
technique, E-matching or trigger-based instantiation,
generates instances when some patterns of terms are present
in the formula. Although it is experimentally quite successful,
it might generate many useless instances. Model-based quantifier
instantiation is a more recent semantic instantiation technique:
instances are built to fix a tentative model that does not agree
with the quantified formulas. An even more recent method to
which we have contributed is conflict-based instantiation; it
can be seen as a weaker and more efficient form of model-based
instantiation, that generates only the instances that contradict
the partial model in the ground solver. Finally, we will also
report on our results on revisiting enumerative instantiation.
These two contributions are joint work with Haniel Barbosa and
Andrew Reynolds.