Crash on SET SESSION gtid_seq_no= DEFAULT

This simple statement crashes the server unconditionally, ouch

SET SESSION gtid_seq_no= DEFAULT;

I think it should instead reverse the effect of any prior SET SESSION gtid_seq_no= 42;