[SMT-LIB] Looking for a tool that can existentialy quantify a single variable

[Ofer Strichman]

Hello there, 
Is anyone aware of a solver that its interface allows to existentially quantify a single variable from a linear arithmetic formula ? 
In other words, given a boolean combination of linear predicates \phi, and a single numeric variable x, returns \exists x. \phi, i.e. \phi after existentially quantifying x ? 

Thanks, 
Ofer