log/smt2perr091.smt2:1:14: first argument of 'ite' is bit-vector of bit-width 2