of the inner loop of Figure \[fig:example\]: $$\begin{aligned}
  {\llbracket {\langle v_4,v_5 \rangle}\cdot {\langle v_5,v_6 \rangle} \rrbracket} &= {\llbracket {\langle v_4,v_5 \rangle} \rrbracket} {\odot}{\llbracket {\langle v_5,v_6 \rangle} \rrbracket}\\
  &={\fbox{$t > 0 \land r'=r-1 \land {\mathit{stable}}(\{q, t, x, y\})$}}\end{aligned}$$ $$\begin{aligned}
  {\llbracket {\langle v_4,v_5 \rangle} \cdot {\langle v_5,v_6 \rangle} \cdot {\langle v_6,v_4 \rangle} \rrbracket} &=
  {\llbracket {\langle v_4,v_5 \rangle} \!\cdot\! {\langle v_5,v_6 \rangle} \rrbracket} {\odot}{\llbracket {\langle v_6,v_4 \rangle} \rrbracket}\\
  &= {\fbox{$t > 0 \land r'=r-1 \land t'=t-1 \land {\mathit{stable}}(\{q, x, y\})$}}\end{aligned}$$

The final step in describing our analysis is to provide a definition of the iteration operator (${\ostar}$) of LRA. The idea behind the definition of the iteration operator is to use an SMT solver to extract recurrence relations from the loop body, and then use the closed form of these recurrences for the abstraction of the loop. We explain this in detail in Section \[sec:lra\]. Here, we illustrate how LRA works on the running example to provide some intuition on the analysis.

After computing a formula ${\varphi}_{\textsf{inner}}$ representing the body of the inner loop (as given above), we apply the iteration operator ${\ostar}$ to compute a formula representing any number of executions of the inner loop. The iteration operator begins by extracting 