Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
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…
cs.LO2021
Interpolation and Model Checking for Nonlinear Arithmetic
Dejan Jovanović, Bruno Dutertre
We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving…