regress/parser/btor2perr000.btor2:4:19: term with id 17 has bit-vector size 7 but expected sort '16' of size 6