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