model: refactor "infeasible" printing

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 0e24f1b0eaa91679726a8e805c6056acf89f824a..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;
 
@@ -516,20 +519,14 @@ static void print_list(action_list_t *list)
 
 void ModelChecker::print_summary(void)
 {
-       if (!isfeasible()) {
-               if (DBG_ENABLED())
-                       printf("INFEASIBLE EXECUTION!\n");
-               else
-                       return;
-       }
-
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
        printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 
-
        scheduler->print();
 
+       if (!isfeasible())
+               printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");
 }