log/smt2perr137.smt2:8:11: expected ')' to close '(_ rotate_right' at 'unexpected_symbol'