To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in SMT(EUF ÈT). - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Alessandro Santuari; Roberto Sebastiani (LPAR, 2006)