void ClockVector::print() const
{
int i;
- printf("CV: (");
+ model_print("CV: (");
for (i = 0; i < num_threads; i++)
- printf("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+ model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
}