From c1cc5e279bcba4216bde88a63dafac96d3ef47ba Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Tue, 2 Oct 2012 18:06:46 -0700 Subject: [PATCH] a bug fix --- model.cc | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) 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(); -- 2.34.1