Fix SMT1 parser :extrasorts/:extrapreds.
Fix operator-printing issue in SMT2.
Merge branch '1.4.x'