  This paper deals with a problem from discrete-time robust control which
requires the solution of constraints over the reals that contain both universal
and existential quantifiers. For solving this problem we formulate it as a
program in a (fictitious) constraint logic programming language with explicit
quantifier notation. This allows us to clarify the special structure of the
problem, and to extend an algorithm for computing approximate solution sets of
first-order constraints over the reals to exploit this structure. As a result
we can deal with inputs that are clearly out of reach for current symbolic
solvers.
