time bug

[Henry Cejtin]

I  would  definitely  vote for getrusage() over times().  My argument is that
the former is in seconds/microseconds while the latter depends on the  length
of  time  in  a  clock tick which is goofy.  This rounding problem could have
caused the problem as Matt said.

Note, the number of tiks per millisecond doesn't have to be an integer and in
fact  historically wasn't.  The traditional value was 60 Hz, so 1000/60 ticks
per millisecond.