I added Bitwuzla support to my GCC translation validator, smtgcc. The performance improvement over Z3 and cvc5 is impressive!
github.com/kristerw/smt...

My talk "Formalizing the Semantics of GIMPLE" at the GNU Cauldron is now available:
conf.gnu-tools-cauldron.org/opo25/talk/M...

Implemented partial assembler support for the SH architecture (used in Sega’s Dreamcast game console) in smtgcc, my GCC translation validator:
github.com/kristerw/smt...

I have implemented support for BPF assembly in the smtgcc GCC translation validator:
github.com/kristerw/smt...

It has already found multiple bugs in the GCC BPF backend. I have reported three so far:
gcc.gnu.org/bugzilla/sho...
gcc.gnu.org/bugzilla/sho...
gcc.gnu.org/bugzilla/sho...

I’ve posted a mid-year update for my GCC translation validation tool, smtgcc, to the GCC mailing list:
gcc.gnu.org/pipermail/gc...

While working on my GCC translation validator, smtgcc, I've encountered several cases where GIMPLE IR semantics are ambiguous or inconsistent with GCC optimizations.

I'll discuss these on the GCC mailing list and link each corresponding thread here. 🧵

I’ve posted an end-of-year update for my GCC translation validation tool, smtgcc, to the GCC mailing list:
gcc.gnu.org/pipermail/gc...