What does a model in ∃x∀y∃z∀u . F[x, y, z, u] mean?

In Playing with Quantified Satisfaction they state as follows:

Evaluating a quantified formula of the form ∃x∀y∃z∀u . F[x, y, z, u] can be naturally seen as a game between two parties: the existential player that seeks to find values for x and z that satisfy F and a universal player (spoiler) that attempts to counter the moves for x with values for y and the move for z with values for u such that falsify F.

The sentence seems natural and logical to me, but suddenly I remember that Z3 only returns a model of the outermost existential variables... so I think that, in that formula, the existential player does not need values of x and z, but only of x.

In other words, a model of that formula will only return values of x. That is, let us consider that ∀y∃z∀u . F[x, y, z, u] is Phi, so isn't our original formula equivalent to ∃x . Phi? That is, the existential player should win with values of x no matter his value of z. What am I missing? What does a model mean in a formula with such quantifier alternation?

Let me first recap what that formula means from the perspective of satisfiability. Let's first skolemize your formula:

 There exists a constant c, and a function G, such that:
       ∀y∀u . F[c, y, G(c), u] 

(Note that this form is not equivalent, but rather equisatisfiable to the original. But in our context of SMT solving, that makes no difference; so I'll ignore that detail.)

Now, if a theorem prover (note: I'm explicitly not saying SMT solver here) finds a falsification of this equisatisfiable formula, it needs to demonstrate a c, and a functionG, s.t. you can always find a y and u that makes the formula F[c, y, G(c), u] false. Note that y and u can (and will) depend on c and G; i.e., different choices of c and G can lead to a different y and u. The onus of the solver is to find a constant c and a function G.

Now, I explicitly said "a theorem prover" above, not an SMT solver. Of course, an SMT solver is a certain kind of a theorem prover; it has tremendous "push-button" powers, but it can't prove everything that is theoretically possible to prove using a full-fledged prover. In particular, it cannot find arbitrary functions like G. Typically, it can find functions that are "finite" mappings, that is, where the function takes only a finite number of values in its range. So, it tries its best, and gives up if it cannot find such a function G. (The keywords here are model-based-quantifier-instantiation, e-matching, and finite model finding; if you want to Google your whole day away!)

So, if the SMT solver finds a falsification of this, it'll display the value of c (which of course is the value of x), and will stop there. A better system can of course display G as well. But note that it'd be terribly confusing, because there's no mention of this G in your original formula, so it's not even clear how to present such a function to the user, or let them access it through your API etc. (Though you can make it compute some of these in simple cases, if you skolemize by hand. I believe we discussed this option in the past.)

Finally, we can address your question. The prover not only has to demonstrate the existence of x but also G, which implicitly defines z via the equality z = G(x). So, your original quote is valid, we need both. It's just that SMT solvers stop at the top-level universal and don't go deeper, for both technical and presentation purposes. If you want to see the G, simply skolemize by hand, and ask for the value of your skolem function G. If you get lucky (i.e., if the problem is simple enough for the solver's heuristics to kick in and find such a G), then you'll get a G. But if G isn't finitely valued, then most likely you'll get unknown as the answer. And that's the price you pay for having a push-button tool.

I hope that clears things up. This paper is a good read on how to perform finite-model-finding in the context of SMT solvers, if you want to learn more. Note that an SMT solver typically wants to be "good" at problems that arise in practice. To that end, there are many choices to make. And the goals of speed, decidability, ease-of-use are all competing when it comes to reasoning in general, and in particular with quantified formulae. Quantifiers are usually handled by an upstream tool, like Dafny, Isabelle, Coq, etc. and they use SMT solvers to discharge proof goals there are typically quantifier free, taking advantage of decision procedures SMT solvers implement for reasoning with numbers, bit-vectors, etc., where SMT solvers shine at.