https://gcc.gnu.org/bugzilla/show_bug.cgi?id=83952
--- Comment #8 from Eyal Rozenberg <eyalroz at technion dot ac.il> --- Andrew, Marc: Sorry for the mess with the other bug. If only Bugzilla had an "edit comment" feature I wouldn't have opened this second one.