=================================================

In this section, we describe the iteration operator of linear recurrence analysis. Suppose that we have a formula ${{\varphi}_{\textsf{body}}}$ which approximates the behaviour of the body of a loop. Our goal is to compute a formula ${{\varphi}_{\textsf{body}}}^{\ostar}$ which represents the effect of zero or more executions of the loop body. Our iteration operator works by extracting recurrence relations from the formula ${{\varphi}_{\textsf{body}}}$ and then computing closed forms for these relations. We present our iteration operator in three stages, based on the types of recurrence relations being considered: *simple recurrence equations*, *stratified recurrence equations*, and *linear recurrence (in)equations*. Simple and stratified recurrences are classical classes of recurrence equations. Linear recurrence (in)equations generalize the class of inequations presented in [@Ancourt2010] by using stratified recurrences to generate polynomial (rather than just linear) inequations. The main conceptual contribution of this section is the idea to use SMT solvers to extract recurrences (and other relevant information) from a loop body formula.

In the remainder of this section, we fix a formula ${{\varphi}_{\textsf{body}}}$ representing the body of a loop. We assume that ${{\varphi}_{\textsf{body}}}$ is expressed in linear (rational and integer) arithmetic; our strategy for dealing with non-linear arithmetic is described in Section \[sec:discussion\]. We also 