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