X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=78729bd38ac4d9da05d25527450f6668f38be997;hb=651e9182baf50ef1e235ad7a587730b989bb44c7;hp=2fabb08291965adfa512930cfbe48d438b05e716;hpb=6f00cf7293dd0b42cad96855604287f6814f36d8;p=c11tester.git

diff --git a/model.cc b/model.cc
index 2fabb082..78729bd3 100644
--- a/model.cc
+++ b/model.cc
@@ -319,11 +319,11 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
-	if (forklock) {
+	if (modellock) {
 		static bool fork_message_printed = false;
 
 		if (!fork_message_printed) {
-			model_print("Fork handler trying to call into model checker...\n");
+			model_print("Fork handler or dead thread trying to call into model checker...\n");
 			fork_message_printed = true;
 		}
 		delete act;
@@ -353,6 +353,8 @@ static void runChecker() {
 
 void ModelChecker::startChecker() {
 	startExecution(get_system_context(), runChecker);
+	snapshot_stack_init();
+	snapshot_record(0);
 }
 
 bool ModelChecker::should_terminate_execution()
@@ -363,6 +365,8 @@ bool ModelChecker::should_terminate_execution()
 	else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
 		execution->set_assert();
 		return true;
+	} else if (execution->isFinished()) {
+		return true;
 	}
 	return false;
 }