regress/parser/smt2perr068.smt2:2:31: index sort of array and sort of index do not match