Quantifier elimination (QE) is a key task in formal verification algorithms,
and the ability to return partial results, such as under-approximations, is beneficial for many QE clients.
In Linear Real Arithmetic (LRA), existing QE methods often fail to preserve syntactic convexity,
that is, they return a disjunction even for a conjunctive input, or they return a large
non-minimal representation. We define the novel concept of Bidirectional Model-Based Projection
and a new QE algorithm for LRA (BMBP-QE) that
(i) returns a conjunctive over-approximation and a disjunctive under-approximation when interrupted early,
(ii) returns a minimal conjunction when the input is conjunctive, and
(iii) applies to arbitrary LRA formulae.
We show that BMBP-QE outperforms SMT-based QE algorithms,
offering improvements in both runtime and result size.