X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=datarace.cc;h=1cc407bb991889545210f54ec313ae84c49cf412;hp=34060faeab2bc2a70515a9f3cc01b5a5d5ebf68e;hb=1be4d40117ac7eb13715f6384c7dfdd390246aa7;hpb=7c003db5218470054490a6777c97c6611b933a12

diff --git a/datarace.cc b/datarace.cc
index 34060fa..1cc407b 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -85,7 +85,8 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
 
 	/* If the race is realized, bail out now. */
 	if (checkDataRaces()) {
-		model->assert_thread();
+		model->set_assert();
+		model->switch_to_master(NULL);
 	}
 }
 
@@ -121,7 +122,7 @@ void printRace(struct DataRace * race) {
 	printf("Datarace detected\n");
 	printf("Location %p\n", race->address);
 	printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
-	printf("Second access: thread %u, iswrite %u\n", race->newaction->get_tid(), race->isnewwrite);
+	printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
 }
 
 /** This function does race detection for a write on an expanded record. */