find arctic matrices via SMT encoding (QF_LRA)