Quantifier elimination with floor functions for parametric Presburger arithmetic

Let $R=\Z[t]$ and $X=\N$. Define

$$\mathcal{L}'_R=\mathcal{L}_R\cup\\{g_{\alpha(t)}:\alpha\in R\\},$$

where each $g_{\alpha(t)}$ is interpreted by

$$g_{\alpha(t)}(x)=\max\\{q\in\Z:q\cdot|\alpha(t)|\leq x\\},$$

with $g_{\alpha(t)}(x)=0$ when $\alpha(t)=0$. Quantifier-elimination conjecture. Every $\mathcal{L}_R$-formula is logically equivalent to a quantifier-free formula in $\mathcal{L}'_R$. The paper presents this as a suggestion motivated by related work, and the supplied text gives no resolution status.