int __libm_dummy(void) { return 42; }