to over-approximate quantifier elimination. Two possibilities are to use Algorithm \[alg:convex\_hull\] to compute the convex hull of $guard({{\varphi}_{\textsf{body}}})$, or to use optimization modulo theories [@Li2014] to compute intervals for each pre- and post-state variable in ${\varphi}_{\textsf{body}}$.

Bringing it all together
------------------------

We close this section by describing how the pieces defined in this section fit into the iteration operator of linear recurrence analysis. We let $\textit{CR}({{\varphi}_{\textsf{body}}})$ denote the set of closed linear recurrence (in)equations (including simple and stratified recurrence equations) satisfied by ${{\varphi}_{\textsf{body}}}$. Each such (in)equation is of the form $\vec{c}\vec{x}^{(k)} \bowtie t$, where the free variables of $t$ are drawn from $\{ x^{(0)} : x \in {\textsf{Var}}\}$ and a distinguished variable $k \notin {\textsf{Var}}$ indicating the loop iteration. We define $${{\varphi}_{\textsf{body}}}^+ {\triangleq}{\fbox{$\exists k. k \geq 1  \land \bigwedge \{ \vec{c}\vec{x'} \bowtie t[\vec{x}^{(0)} \mapsto \vec{x}] : \vec{c}\vec{x}' \bowtie t \in \textit{CR}({{\varphi}_{\textsf{body}}}) \}$}}$$ where $t[\vec{x}^{(0)} \mapsto \vec{x}]$ denotes the term $t$ with every variable of the form $x^{(0)}$ is replaced by the corresponding variable $x$.

Finally, our iteration operator is defined as: $${{\varphi}_{\textsf{body}}}^{\ostar}{\triangleq}{\fbox{$({{\varphi}_{\textsf{body}}}^+ \land \textit{guard}({{\varphi}_{\textsf{body}}})) \lor \bigwedge_{x \in {\textsf{Var}}} x' = x.$}}$$

Linearization {#sec:discussion}
=============

The iteration operator presented in the previous section relies heavily on using an SMT solver to 