regress/parser/smt2perr114.smt2:1:25: expected terms of same sort at indices 0 and 1 as argument to 'bvand'