An SMT Formalization of Mixed-Precision Matrix Multiplication