  Quantifier elimination (QE) is an important problem that has numerous
applications. Unfortunately, QE is computationally very hard. Earlier we
introduced a generalization of QE called $\mathit{partial}$ QE (or PQE for
short). PQE allows to unquantify a $\mathit{part}$ of the formula. The appeal
of PQE is twofold. First, many important problems can be solved in terms of
PQE. Second, PQE can be drastically faster than QE if only a small part of the
formula gets unquantified. To make PQE practical, one needs an algorithm for
verifying the solution produced by a PQE solver. In this paper, we describe a
very simple SAT-based verifier called $\mathit{VerPQE}$ and provide some
experimental results.
