Z3 has difficult ematching over arithmetic expressions. Abstracting them to uninterpreted functions can help.