ex_a.smt 84 Bytes