// Object id mangling routines
void mangle(int in, unsigned char& out1, unsigned char& out2,
	    unsigned char& out3);
int demangle(unsigned char in1, unsigned char in2, unsigned char in3);