log/smt2perr114.smt2:1:10: first argument of 'bvand' is bit-vector of width 1 but argument 2 is a bit-vector of width 2