regress/parser/smt2perr115.smt2:2:16: expected bit-vector term at index 0 as argument to 'bvand'