From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 May 2012 18:09:07 +0000 (-0700)
Subject: model: print replay/divergence information when starting a new execution
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e88424edbf9ec1ff1df8e83e10a317dae3704628;p=cdsspec-compiler.git

model: print replay/divergence information when starting a new execution
---

diff --git a/model.cc b/model.cc
index 976b395..6fea489 100644
--- a/model.cc
+++ b/model.cc
@@ -116,12 +116,20 @@ thread_id_t ModelChecker::advance_backtracking_state()
 
 bool ModelChecker::next_execution()
 {
+	DBG();
+
 	num_executions++;
 	print_summary();
 	if ((exploring = model->get_next_backtrack()) == NULL)
 		return false;
 	model->reset_to_initial_state();
 	nextThread = get_next_replay_thread();
+
+	if (DBG_ENABLED()) {
+		printf("Next execution will diverge at:\n");
+		exploring->get_diverge()->print();
+		print_list(exploring->get_trace());
+	}
 	return true;
 }