LOMay 25
Nonlinear Arithmetic with SMTLIB Division is Undecidable
arXiv:2605.261816.4
Predicted impact top 55% in LO · last 90 daysOriginality Incremental advance
AI Analysis
This result reveals a fundamental limitation in a widely-used standard for SMT solvers, affecting researchers and practitioners relying on SMTLIB-compliant tools.
The paper proves that the nonlinear real arithmetic theory (NRA) as defined in the SMTLIB standard is undecidable due to the treatment of division by zero as an uninterpreted function, which enables encoding integer arithmetic problems.
We show that the nonlinear real arithmetic theory (NRA) as defined in the SMTLIB standard is undecidable. The undecidability arises from the treatment of division by zero as an uninterpreted function, which allows encoding integer arithmetic problems into NRA formulas.