What is the state-of-the-art solver for quantifier elimination under LRA?

Question

I've tried Z3 on quantifier elimination under linear real arithmetic. The formula isn't very large but when the number of variables to eliminate exceeds 5, it takes very long (or never terminates). Does there exist any other solvers that can do better? Or is there any trick that can help Z3?

Answer 1

I am not an expert but you could try with RedLog of Reduce.