Fix SMT1 parser :extrasorts/:extrapreds.
Fix operator-printing issue in SMT2.