SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far. However, in the context of program verification, polynomials are often insufficient to capture the behavior of the analyzed system without resorting to approximations. In the last years, incremental linearization has been applied successfully to satisfiability modulo real arithmetic with transcendental functions. We adapt this approach to an extension of polynomial integer arithmetic with exponential functions. Here, the key challenge is to compute suitable lemmas that eliminate the current model from the search space if it violates the semantics of exponentiation. An empirical evaluation of our implementation shows that our approach is highly effective in practice.

翻译：SMT求解器采用复杂技术处理多项式（线性或非线性）整数算术。相比之下，非多项式整数算术迄今基本被忽视。然而在程序验证领域，若不作近似处理，多项式往往难以完全刻画被分析系统的行为特征。近年来，增量线性化方法已成功应用于含超越函数的实数算术可满足性判定。我们将该思路拓展至含指数函数的扩展多项式整数算术场景。此处核心挑战在于：当当前模型违反幂运算语义时，如何构造恰当的引理将其从搜索空间中消除。实验评估表明，我们的方法在实际应用中展现出显著有效性。