A classical theorem in Integer Programming by Lenstra says that any integer system $$A x \le b$$ can be solved in polynomial time, where $A \in \mathbb{Z}^{m \times n}, x \in \mathbb{Z}^n, b \in \mathbb{Z}^m$. Here we fix the dimension $n$ of the variables to be solved over (it would be NP-complete to solve for $n$ arbitrary).
Viewed under the the lense of logic/computational complexity, this theorem says that any existential statement $$ \exists x \in \mathbb{Z}^n : \Phi(x)$$ can be decided in polynomial time, where $\Phi$ is a formula in Presburger arithmetic.
By the work of Semenov, we also know that Presburger arithmetic with added precidates, such as "x is a power of 2", or "x is a Fibonacci number" is decidable.
Question: For $n$ fixed, can we decide in polynomial time sentences of the form $$\exists x \in \mathbb{Z}^n : \Psi(x)$$ where $\Psi(x)$ is a Presburger formula, augmented with some the Fibonacci (or Power of 2) predicates?
Example: Does the following system have a solution?
$$ \begin{cases} 3x_1 + 2x_2 \le 1000 \\ 17x_2 - x_1 \le 5 \\ 2x_1 + 5x_2 \quad \text{is a power of 2} \end{cases} $$
