int printf(const char *format, ...);


int
arg1(int a1,int a2,int a3,int a4)
{
    printf("#0006:%d %d %d %d\n",a1,a2,a3,a4);
}

int
arg0(int a1,int a2,int a3,int a4)
{
    arg1(0,1,2,3);
    printf("#0013:%d %d %d %d\n",a1,a2,a3,a4);
}

main()
{
    arg0(0,1,2,3);
    return 0;
}