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} $$