Currently Yices2 lacks optimized handling of Formulas defined over finite fields. This is especially annoying when operating over elliptical curves.