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 468900a..c4bc693 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;
                /*