  Let $\mathcal{L}_{\mathcal{X}}$ be the language of first-order, decidable
theory $\mathcal{X}$. Consider the language,
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$, that extends
$\mathcal{L}_{\mathcal{X}}$ with formulas of the form $\forall x \in A: \phi$
(restricted universal quantifier, RUQ) and $\exists x \in A: \phi$ (restricted
existential quantifier, REQ), where $A$ is a finite set and $\phi$ is a formula
made of $\mathcal{X}$-formulas, RUQ and REQ. That is,
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ admits nested restricted quantifiers.
In this paper we present a decision procedure for
$\mathcal{L}_{\mathcal{RQ}}(\mathcal{X})$ based on the decision procedure
already defined for the Boolean algebra of finite sets extended with restricted
intensional sets ($\mathcal{L}_\mathcal{RIS}$). The implementation of the
decision procedure as part of the $\{log\}$ (`setlog') tool is also introduced.
The usefulness of the approach is shown through a number of examples drawn from
several real-world case studies.
