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.

diff --git a/model.cc b/model.cc
index 468900aeb6120f659124e09fc839ac8aa53416ee..c4bc693ef5560f646684b3a2cb002e685f4be848 100644 (file)
--- 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;
                /*