  In this paper we introduce a novel quantifier elimination method for
conjunctions of linear real arithmetic constraints. Our algorithm is based on
the Fourier-Motzkin variable elimination procedure, but by case splitting we
are able to reduce the worst-case complexity from doubly to singly exponential.
The adaption of the procedure for SMT solving has strong correspondence to the
simplex algorithm, therefore we name it FMplex. Besides the theoretical
foundations, we provide an experimental evaluation in the context of SMT
solving.
