log/smt2perr115.smt2:2:16: argument 1 of 'bvand' is an array