model: one release sequence may help resolve another
[model-checker.git] / model.cc
index e3d26d3..38f40e5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1311,6 +1311,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                }
 
                if (updated) {
+                       /* Re-check all pending release sequences */
+                       work_queue->push_back(CheckRelSeqWorkEntry(NULL));
                        /* Re-check act for mo_graph edges */
                        work_queue->push_back(MOEdgeWorkEntry(act));