log/smt2perr046.smt2:1:36: expected bit-width at 'symbol'