embarrassing bug...fixed...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 2aaa1c26dbea3ad9e78720683635a117d83243f1..e5926730b87c512b388e058a23f08e031a5df33a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1509,8 +1509,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                                continue;
                        }
 
-                       /* Only writes can break release sequences */
-                       if (!act->is_write())
+                       /* Only non-RMW writes can break release sequences */
+                       if (!act->is_write() || act->is_rmw())
                                continue;
 
                        /* Check modification order */
@@ -1815,6 +1815,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
                                act->is_read() &&
                                !act->could_synchronize_with(curr) &&
                                !act->same_thread(curr) &&
+                               act->get_location() == curr->get_location() &&
                                promise->get_value() == curr->get_value()) {
                        curr->get_node()->set_promise(i);
                }