Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers

Cristina Borralleras, Daniel Larraz, Albert Oliveras +2

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 decid…