[Clc-crux64] Bugs in 32-bit-code.