From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 May 2012 21:01:58 +0000 (-0700)
Subject: model: bugfix - rearrange debug message
X-Git-Tag: pldi2013~462
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a89a58d94e8ef32d5e446c33be020e8ce885a387;p=model-checker.git

model: bugfix - rearrange debug message

This debug message depends on 'exploring' still being a valid reference.
However, we immediately explore one step via get_next_replay_thread(), which
could discard this Backtrack object. So print the debug message before doing
any exploration of the next execution stage.
---

diff --git a/model.cc b/model.cc
index 7a29e00..aba3e8b 100644
--- a/model.cc
+++ b/model.cc
@@ -142,14 +142,15 @@ bool ModelChecker::next_execution()
 	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());
 	}
+
+	model->reset_to_initial_state();
+	nextThread = get_next_replay_thread();
 	return true;
 }