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