Is the feasibility of a system of non-convex quadratic equations and inequations decidable?

I would like to know whether the following problem is decidable.

Given the following system in $$x \in [0,1]^n$$

$$x^T Q_i x + r_i = 0 \mbox{ for } i = 1, ..., k$$

$$x^T Q_j x + r_j \neq 0 \mbox{ for } j = k+1, ..., t$$

where $$r_i, r_j \in [0,1]$$ are rational constants and $$Q_i, Q_j$$ are symmetric indefinite $$n \times n$$ matrices, decide whether this system is feasible.

According to me (after a series of transformations and added slack variables), the decidability problem above is equivalent to asking whether the global maximum of $$q_j^T x$$ (a linear term) can be found, subject to non-linear, non-convex quadratic constraints

$$x^T Q_i x + q_i^T x + r_i \leq 0 \mbox{ for } i = 1, ..., u$$

where $$x$$, $$r_i$$ and $$Q_i$$ have the same form as before (but are not identical), $$q_i$$ is a column vector of length $$n$$, and $$q_i^T$$ is the transpose of $$q_i$$.

The latter formulation of the problem can be viewed as a Quadratically Constrained Quadratic Program (QCQP), except that the objective function is linear. And the constraints are, in general, non-linear. Also note that the latter problem is posed as a decision problem, not purely an optimization problem.

Does either one of these problems have a decidability result?

For any fixed $n,k,t$, the feasibility question is a first-order formula in the language of real-closed fields; it would have the components of $x$ as existentially quantified variables and the $r$'s and the entries of the $Q$'s as free variables. Tarski's quantifier elimination theorem for real-closed fields converts this to a propositional combination of equations and inequalities for the free variables. The quantifier-elimination is algorithmic. So as long as the components of the $Q$'s are given in such a way that you can algorithmically do arithmetic with them, the feasibility question is decidable.