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