(void)state; (void)current;
	(void)s1; (void)s2;

/*
STDC(0)
*/