Let $p$ be a prime number. Consider the abelian group $p^{-\infty} {\mathbb Z} = \bigcup p^{-n} {\mathbb Z}$ consisting of rational numbers whose denominator is a power of $p$, under addition.

View ${\mathbb Z}$ as a predicate on $p^{-\infty} {\mathbb Z}$, in the sense that ${\mathbb Z}(x)$ is true if $x$ is an integer.

Let $\phi$ be the function from ${\mathbb Z}$ to $p^{-\infty} {\mathbb Z}$ given by $\phi(n) = p^n$.

Is the first order theory of $( p^{-\infty} {\mathbb Z}, =, >, 0, 1, +, {\mathbb Z}, \phi )$ decidable?

A bit of background: The theory of $({\mathbb Z}, =, >, 0, 1, +, \phi)$ is decidable (where here $\phi$ is restricted to natural numbers). This is a result of Semenov; see my answer to the question Beyond Presburger Arithmetic for more.

On the other hand, what I've described is pretty close to undecidable theories. If I included a predicate $f: {\mathbb Z} \times p^{-\infty} {\mathbb Z} \rightarrow p^{-\infty} {\mathbb Z}$ sending $(n,x)$ to $2^n \cdot x$, it would be undecidable by a result of Delon ("${\mathbb Q}$ Muni de l'Arithmetique Faible de Penzin est Decidable," Proc. of AMS, vol. 125, no 9, 1997).

Any references or results would be greatly appreciated.