model: bugfix - infinite loop in resolve_release_sequences()

diff --git a/model.cc b/model.cc
index 64c1daa5d8f2b52aa561b50cbd2a07a65853ec84..0283911b6eea07e57c7b7266fe3c80fc2d755595 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1233,7 +1233,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
 
                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator it = action_trace->rbegin();
 
                        /* propagate synchronization to later actions */
                        action_list_t::reverse_iterator it = action_trace->rbegin();

-                       while ((*it) != act) {
+                       for (; (*it) != act; it++) {

                                ModelAction *propagate = *it;
                                if (act->happens_before(propagate)) {
                                        propagate->synchronize_with(act);
                                ModelAction *propagate = *it;
                                if (act->happens_before(propagate)) {
                                        propagate->synchronize_with(act);