log/smt2perr072.smt2:1:23: argument 2 of '=>' is a bit-vector of width 2