From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 3 Oct 2012 01:06:46 +0000 (-0700)
Subject: a bug fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c1cc5e279bcba4216bde88a63dafac96d3ef47ba;p=cdsspec-compiler.git

a bug fix
---

diff --git a/model.cc b/model.cc
index ae0a787..0006fd6 100644
--- a/model.cc
+++ b/model.cc
@@ -139,6 +139,9 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 	ModelAction *next = node_stack->get_next()->get_action();
 
 	if (next == diverge) {
+		if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+			earliest_diverge=diverge;
+
 		Node *nextnode = next->get_node();
 		/* Reached divergence point */
 		if (nextnode->increment_promise()) {
@@ -158,8 +161,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			Node *node = nextnode->get_parent();
 			tid = node->get_next_backtrack();
 			node_stack->pop_restofstack(1);
+			if (diverge==earliest_diverge) {
+				earliest_diverge=node->get_action();
+			}
 		}
 		DEBUG("*** Divergence point ***\n");
+
 		diverge = NULL;
 	} else {
 		tid = next->get_tid();
@@ -198,9 +205,6 @@ bool ModelChecker::next_execution()
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
 
-	if (earliest_diverge == NULL || *diverge < *earliest_diverge)
-		earliest_diverge=diverge;
-
 	if (DBG_ENABLED()) {
 		printf("Next execution will diverge at:\n");
 		diverge->print();