  We present a general simplification of quantified SMT formulas using variable
elimination. The simplification is based on an analysis of the ground terms
occurring as arguments in function applications. We use this information to
generate a system of set constraints, which is then solved to compute a set of
sufficient ground terms for each variable. Universally quantified variables
with a finite set of sufficient ground terms can be eliminated by instantiating
them with the computed ground terms. The resulting SMT formula contains
potentially fewer quantifiers and thus is potentially easier to solve. We
describe how a satisfying model of the resulting formula can be modified to
satisfy the original formula. Our experiments show that in many cases, this
simplification considerably improves the solving time, and our evaluations
using Z3 and CVC4 indicate that the idea is not specific to a particular
solver, but can be applied in general.
