*** catbtor: parse error in 'andargmismatch.in' line 6: expected bitvec of size 3 for first argument but got 1