[gecode-users] printing of time in script.cpp

[Jan Kelbel]

Hi,

I found some non-correct behavior in function
void stop(Support::Timer& timer, std::ostream& os)
lines 57 to 67 in release 3.7.1 in file gecode\driver\script.cpp
When for example (o_hour > 0) and (o_min == 0), then the result of the 
output is o_hour:o_sec.o_msec, and the minute part is skipped.

Possibly, the lines 59 and 60 can be replaced by:

if (o_hour) {
  os << o_hour << ":";
  if (0 == o_min) {
    os << "00:";
    os.width(2); os.fill('0');
  }
}

Cheers,
        Jan


_______________________________________________
Gecode users mailing list
users@gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users