fixed type eror in 21.tst.smt2