EUF${}^n$: A Decidable Extension to the Theory of Equality with Uninterpreted Functions

Yide Du, Zhenbang Chen, Weijiang Hong +1

The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations,…