Nonlinear Arithmetic with SMTLIB Division is Undecidable

Dejan Jovanovic

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