log/smt2perr051.smt2:1:38: expected ')' to close bit-vector sort at 'symbol'