*** catbtor: parse error in 'arrayasbv.in' line 6: expected bitvec sort for first argument of add