X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=cf845ecd215a68a83c3ca1a449c7f06cf557a808;hp=0e24f1b0eaa91679726a8e805c6056acf89f824a;hb=99c0d85ef14259735fdd84cb7b3e578f64434314;hpb=187f2106785fe1ea4d34b0aee54d68468630675e

diff --git a/model.cc b/model.cc
index 0e24f1b0..cf845ecd 100644
--- 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");
 }