> This is the last patch needed to get make check happy when using
> gcc -fsanitize=undefined. Please do push it (or one of the variants
> discussed in the thread).

Pushed.