  We propose a new quantifier elimination algorithm for the theory of linear
real arithmetic. This algorithm uses as subroutine satisfiability modulo this
theory, a problem for which there are several implementations available. The
quantifier elimination algorithm presented in the paper is compared, on
examples arising from program analysis problems, to several other
implementations, all of which cannot solve some of the examples that our
algorithm solves easily.
