regress/parser/smt2perr079.smt2:3:16: expected terms of same sort at indices 1 and 2 as argument to '='