X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=33e8805078b546ac8d1b4f87dab3ea31e9be2651;hb=ecf16617a0c289981925fcd2437595f3a2fce8fe;hp=ab16bf82528ea5ebf30766970b37faca5a6ada1f;hpb=122aad1259a2df612ad39c640551be8da9cb26b9;p=model-checker.git

diff --git a/model.cc b/model.cc
index ab16bf8..33e8805 100644
--- a/model.cc
+++ b/model.cc
@@ -446,8 +446,8 @@ bool ModelChecker::next_execution()
 		if (is_deadlocked())
 			assert_bug("Deadlock detected");
 
-		print_bugs();
 		checkDataRaces();
+		print_bugs();
 		printf("\n");
 		print_stats();
 		print_summary();
@@ -917,8 +917,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 	}
 
 	/* See if we have realized a data race */
-	if (checkDataRaces())
-		assert_bug("Data race");
+	checkDataRaces();
 }
 
 /**
@@ -1849,8 +1848,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 	}
 
 	// If we resolved promises or data races, see if we have realized a data race.
-	if (checkDataRaces())
-		assert_bug("Data race");
+	checkDataRaces();
 
 	return updated;
 }