  We present new methods for solving the Satisfiability Modulo Theories problem
over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA),
which consists in deciding the satisfiability of ground formulas with integer
polynomial constraints. Following previous work, we propose to solve
SMT(QF-NIA) instances by reducing them to linear arithmetic: non-linear
monomials are linearized by abstracting them with fresh variables and by
performing case splitting on integer variables with finite domain. For
variables that do not have a finite domain, we can artificially introduce one
by imposing a lower and an upper bound, and iteratively enlarge it until a
solution is found (or the procedure times out).
  The key for the success of the approach is to determine, at each iteration,
which domains have to be enlarged. Previously, unsatisfiable cores were used to
identify the domains to be changed, but no clue was obtained as to how large
the new domains should be. Here we explain two novel ways to guide this process
by analyzing solutions to optimization problems: (i) to minimize the number of
violated artificial domain bounds, solved via a Max-SMT solver, and (ii) to
minimize the distance with respect to the artificial domains, solved via an
Optimization Modulo Theories (OMT) solver. Using this SMT-based optimization
technology allows smoothly extending the method to also solve Max-SMT problems
over non-linear integer arithmetic. Finally we leverage the resulting
Max-SMT(QF-NIA) techniques to solve $\exists \forall$ formulas in a fragment of
quantified non-linear arithmetic that appears commonly in verification and
synthesis applications.
