Complete Trigger Selection in Satisfiability modulo first-order Theories

Christopher Lynch, Stephen Miner

Let T be an SMT solver with no theory solvers except for Quantifier Instantiation. Given a set of first-order clauses S saturated by Resolution (with a valid literal selection func…