regress/parser/smt2perr080.smt2:3:14: expected terms of same sort at indices 0 and 1 as argument to '='