#include int non_main() { printf("%d", 42); return 0; }