extract information from loop body formulas. This strategy requires that loop body formulas are expressed in a decidable theory which is supported by SMT solvers (in particular, linear arithmetic). However, a program may contain non-linear instructions, and even if it does not, our iteration operator may introduce non-linearity (consider Example \[fig:example\], where the transition formula for the outer loop ${\varphi}_{\textsf{outer}}^{\ostar}$ contains the non-linear proposition $r' =
x-q'y$). Our solution to this problem is to *linearize* non-linear formulas before passing them to the iteration operator.

Linearization is an operation that, given an (arbitrary) arithmetic formula ${\varphi}$, computes a formula $\textit{lin}({\varphi})$ which over-approximates ${\varphi}$ (i.e., ${\varphi}\Rightarrow \textit{lin}({\varphi})$), but which is expressed in linear arithmetic. There is generally no best approximation of a non-linear formula as a linear formula, so our method is (necessarily) a heuristic.

We explain our linearization algorithm informally using an example. Consider the following non-linear formula (where $w,x,y,z$ are integers): $$\psi {\triangleq}1 \leq w = x < y < 5 \land w * y \leq z \leq x * y$$ Our algorithm begins by normalizing $\psi$, separating it into a linear part and a set of non-linear equations (introducing existentially quantified temporary variables as necessary). For example, the result 