Use a standard macro for 64 bit printf conversion specifiers

This avoids duplicating the printf line with an ifdef every
time a 64 bit number needs to be printed.