model: one release sequence may help resolve another

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index e3d26d3261968ca4b4eefd3fd593767045b0687b..38f40e5cd1ee55b47103883fa9677b6ad7ea7e6d 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) {
                }
 
                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));
 
                        /* Re-check act for mo_graph edges */
                        work_queue->push_back(MOEdgeWorkEntry(act));