model: one release sequence may help resolve another
authorBrian Norris <banorris@uci.edu>
Wed, 26 Sep 2012 00:00:53 +0000 (17:00 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 3 Oct 2012 01:31:22 +0000 (18:31 -0700)
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));