#include int __debug_level = 2; int main(void) { double val = 0.0001; printf("%g\n", val); return(0); }