  In this paper we extend a decision procedure for the Boolean algebra of
finite sets with cardinality constraints ($\mathcal{L}_{\lvert\cdot\rvert}$) to
a decision procedure for $\mathcal{L}_{\lvert\cdot\rvert}$ extended with set
terms denoting finite integer intervals ($\mathcal{L}_{[\,]}$). In
$\mathcal{L}_{[\,]}$ interval limits can be integer linear terms including
\emph{unbounded variables}. These intervals are a useful extension because they
allow to express non-trivial set operators such as the minimum and maximum of a
set, still in a quantifier-free logic. Hence, by providing a decision procedure
for $\mathcal{L}_{[\,]}$ it is possible to automatically reason about a new
class of quantifier-free formulas. The decision procedure is implemented as
part of the $\{log\}$ tool. The paper includes a case study based on the
elevator algorithm showing that $\{log\}$ can automatically discharge all its
invariance lemmas some of which involve intervals.
