I pushed a branch containing "hopefully" standard compliant overflow checks. Its in arne/of. I had to change a few places outside of bignum.h in order to get it all working with inlines.
The switch from macro to inlines actually changed semantics, since the INT_TYPE_* macros were actually used both with int and unsigned int. Naturally, the inline functions fail to detect an overflow there, since INT_TYPE is 64 bit and calculations do not overflow.
Maybe someone can try to compile and run verify on something other than amd64 with gcc?
arne