Complexity one-alternation SMT
The question of truth in Presburger Arithmetic with bounded quantifier alternation has been answered with quite some precision by Reddy and Loveland:

C.R. Reddy &amp; D.W. Loveland: Presburger Arithmetic with Bounded Quantifier Alternation.

The paper may be found here (sorry for the ugly link). Their main result is stated as follows:


  The membership in $\mathrm{PA}(m)$ (where $m$ is the number of quantifier alternations) of length $n$ can be decided within space
  $$ 2^{dn^{m+4}}$$
  and in (deterministic) time
  $$ 2^{2^{en^{m+4}}}$$
  Where $d$ and $e$ are constants.


Taking $m=2$, this seems to give at least an upper bound on what you want, and I suspect it's not far from tight, as you have almost full Presburger atomic formulas "at the root".