Тестирование корректности работы компилятора

https://bronevichok.ru/posts/highload-2022.html
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=106523
В докладе упоминается баг в GNU GCC:

    unsigned char f7 (unsigned char x, unsigned int y)
    { return (x << y) | (x >> ((-y) & 7)) }

где программа будет по разному отрабатывать. Бага до сих пор не закрыта.

А вообще для меня там всё магией является (до подобного не дорос, не
факт что дорасту когда-либо), хотя про технологии и инструменты слышал.
Чтобы понять не сломала ли оптимизация компилятора чего, то берётся
получающийся на этапе JIT-а IR-код, преобразуется в SMT-формулу, затем
подаётся в SMT-решатель, который оценивает идентичны ли результаты до и
после оптимизации.