regress/parser/btor2perr005.btor2:5:10: terms with mismatching sort