From 99ca0039c04d8c3dc000f7d3899d1d81564bc168 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 1 Oct 2012 17:20:34 -0700 Subject: [PATCH] model: always re-calculate clock vectors Clock vectors are mutable, via synchronization. We will need to both snapshot and recompute clock vectors as they are generated. Right now, we have some incorrect assumptions in place. This bugfix prevents stale clock vectors (from previous executions) from polluting subsequent executions. --- model.cc | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/model.cc b/model.cc index 468900ae..c4bc693e 100644 --- a/model.cc +++ b/model.cc @@ -543,10 +543,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) /* Discard duplicate ModelAction; use action from NodeStack */ delete curr; - /* If we have diverged, we need to reset the clock vector. */ - if (diverge == NULL) { - newcurr->create_cv(get_parent_action(newcurr->get_tid())); - } + newcurr->create_cv(get_parent_action(newcurr->get_tid())); } else { newcurr = curr; /* -- 2.34.1