void debug_print_trace (int);