  Universal quantifiers occur frequently in proof obligations produced by
program verifiers, for instance, to axiomatize uninterpreted functions and to
express properties of arrays. SMT-based verifiers typically reason about them
via E-matching, an SMT algorithm that requires syntactic matching patterns to
guide the quantifier instantiations. Devising good matching patterns is
challenging. In particular, overly restrictive patterns may lead to spurious
verification errors if the quantifiers needed for a proof are not instantiated;
they may also conceal unsoundness caused by inconsistent axiomatizations. In
this paper, we present the first technique that identifies and helps the users
remedy the effects of overly restrictive matching patterns. We designed a novel
algorithm to synthesize missing triggering terms required to complete a proof.
Tool developers can use this information to refine their matching patterns and
prevent similar verification errors, or to fix a detected unsoundness.
