BDD based procedures for a theory of equality with uninterpreted functions
scientific article; zbMATH DE number 1908515