A Quantifier Elimination Algorithm for Linear Real Arithmetic

We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutines satisfiability modulo this theory and polyhedral projection; there are good algorithms and implementations for both of these. The quantifier elimination al-gorithm presented in the paper is compared, on examples arising from program analysis problems and on random examples, to several other im-plementations, all of which cannot solve some of the examples that our algorithm solves easily.