can we recover this type of information from a loop body formula?

We define the *guard* of a transition formula ${\varphi}$ as follows: $$guard({\varphi}) {\triangleq}{\fbox{$(\exists {\textsf{Var}}. {\varphi}) \land (\exists {\textsf{Var}}'. {\varphi})$}}$$ If ${\varphi}$ is a loop body formula, then $guard({\varphi})$ is a formula which over-approximates the effect of executing *at least one* execution of the loop. Intuitively, $(\exists {\textsf{Var}}. {\varphi})$ as a precondition that must hold before every iteration of the loop and $(\exists {\textsf{Var}}'. {\varphi})$ as a post-condition of the loop that must hold after each iteration.

Consider again the example loop in Section \[sec:stratified\], we have the following loop body formula $${\varphi}_{\textsf{body}} = {\fbox{$x \leq 10 \land x' = x + 1 \land y' = y + x' \land z' = 2x'$}}$$ We compute $guard({\varphi}_{\textsf{body}})$ as follows: $$\begin{aligned}
  guard({\varphi}_{\textsf{body}}) &= {\fbox{$(\exists \texttt{x},\texttt{y},\texttt{z}. {\varphi}_{\textsf{body}}) \land (\exists \texttt{x'},\texttt{y'},\texttt{z'}. {\varphi}_{\textsf{body}})$}} \\
  &\equiv {\fbox{$(\texttt{x} \leq 10) \land (\texttt{x'} \leq 11 \land \texttt{z} = 2\texttt{x'})$}}\ ,\end{aligned}$$ and thereby recover the desired information about `x` and `z`.

Since loop body formulas may be large, it may be adventageous in practice to simplify the guard formula by eliminating the quantifiers (as we did above). A second option, which is more efficient but less precise, is 