*** catbtor: parse error in 'andoutmismatch.in' line 5: expected bitvec of size 1 for first argument but got 32