The ability of program-analysis tools to identify program invariants is hampered by the capabilities of present-day solvers for handling non-linear arithmetic—including polynomials, exponentials, and logarithms. Improved capabilities for reasoning about non-linear functions would help program analyzers establish important program invariants. For instance, reasoning about exponentials provides a way to find invariants of digital-filter programs; reasoning about polynomials and/or logarithms is needed for establishing invariants that describe the time or memory usage of many well-known algorithms. This paper describes the techniques used in an arithmetic-reasoning kit to represent logarithmic and exponential relationships indirectly, using uninterpreted-function symbols and integrity constraints. It also describes a recurrence-relation solver—used to find invariants of loops—that handles two classes of recurrences: * Ones of the form $x_{n+1} = b*x_n + f(n)$, where $b$ is a constant, and $f(n)$ is a sum of polynomials, exponentials, or products of a polynomial and an exponential. * Ones of the form $\mathbf{y_{n+1}} = \mathbf{A}\mathbf{y_n} + \mathbf{f(n)}$, where $\mathbf{y_n}$ is a vector of variables, $\mathbf{A}$ is a rational matrix, and $\mathbf{f(n)}$ is a vector of functions, where each entry is a sum of polynomials, exponentials, or products of a polynomial and an exponential.

Our technique has been implemented in a program analyzer that can analyze general loops—including loops that contain branches and nested loops—and mutually recursive functions. Our experiments show that our technique shows promise for non-linear assertion-checking and resource-bound generation.