schedule: only print when DEBUG is enabled

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 85ad11aacbf9b255a8372b11e82fc1ad8ad74a7e..fc0f13d886bfb6e0139c6f5999b0bd0aaf1becaf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -214,7 +214,7 @@ void ModelChecker::print_trace(void)
 
        scheduler->print();
 
-       printf("\nTrace:\n\n");
+       printf("Trace:\n\n");
 
        for (it = action_trace->begin(); it != action_trace->end(); it++) {
                DBG();