assume that ${{\varphi}_{\textsf{body}}}$ is satisfiable (if it is not, then we can take ${{\varphi}_{\textsf{body}}}^{\ostar}$ to be $\bigwedge_{x \in {\textsf{Var}}} x' = x$, which represents zero iterations of the loop).

Simple recurrence equations
---------------------------

We start by defining simple recurrences and induction variables.

A simple recurrence for a formula ${\varphi}$ is an equation of the form $x' = x +
c$ (for a constant $c$) such that ${\varphi}\models x' = x + c$. If $x' = x + c$ is a simple recurrence for ${\varphi}$, we say that $x$ *satisfies* the recurrence $x' = x + c$, and if there is some $c$ such that $x$ satisfies the recurrence $x' = x + c$, we say that $x$ is an *induction variable*.

Simple recurrences can be detected by first querying an SMT solver for a model $m$ of ${{\varphi}_{\textsf{body}}}$, and then asking whether ${{\varphi}_{\textsf{body}}}$ implies $x' =
x + {{\llbracket x'-x \rrbracket}^{m}}$ (where ${{\llbracket x'-x \rrbracket}^{m}}$ denotes the interpretation of the term $x'-x$ in the model $m$). This implication holds iff $x$ is an induction variable.

If $x$ is an induction variable that satisfies the recurrence $x' = x + c$, then the closed form for $x$ is $x^{(k)} = x^{(0)} 