model: refactor "infeasible" printing
[c11tester.git] / model.cc
index 31809918361c185cedc7d1ac791044f01bd23bad..cf845ecd215a68a83c3ca1a449c7f06cf557a808 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -162,7 +162,10 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
-       print_summary();
+
+       if (isfeasible() || DBG_ENABLED())
+               print_summary();
+
        if ((diverge = model->get_next_backtrack()) == NULL)
                return false;
 
@@ -519,11 +522,11 @@ void ModelChecker::print_summary(void)
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
        printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-       if (!isfeasible())
-               printf("INFEASIBLE EXECUTION!\n");
 
        scheduler->print();
 
+       if (!isfeasible())
+               printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");
 }