  We consider the problem of synthesizing provably non-overflowing integer
arithmetic expressions or Boolean relations among integer arithmetic
expressions. First we use a numerical abstract domain to infer numerical
properties among program variables. Then we check if those properties guarantee
that a given expression does not overflow. If this is not the case, we
synthesize an equivalent, yet not-overflowing expression, or we report that
such an expression does not exists.
  The synthesis of a non-overflowing expression depends on three, orthogonal
factors: the input expression (e.g., is it linear, polynomial,... ?), the
output expression (e.g., are case splits allowed?), and the underlying
numerical abstract domain - the more precise the abstract domain is, the more
correct expressions can be synthesized.
  We consider three common cases: (i) linear expressions with integer
coefficients and intervals; (ii) Boolean expressions of linear expressions; and
(iii) linear expressions with templates. In the first case we prove there
exists a complete and polynomial algorithm to solve the problem. In the second
case, we have an incomplete yet polynomial algorithm, whereas in the third we
have a complete yet worst-case exponential algorithm.
