What is the complexity of the theory of addition (Presburger arithmetic) augmented by a unary predicate that recognizes powers of 2?

The theory of the natural numbers with addition and $x\mapsto 2^x$ is decidable. One reference is the CherlinPoint paper "On extensions of Presburger arithmetic". It can be found on Francoise Point's webpage: http://www.logique.jussieu.fr/~point/papiers/cherlin_point86.pdf 

