#include #include int32_t put_i32(int32_t x) { printf("%d\n", x); return 0; }