X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=508f3b98284920860c9ce5eb4231b786b070b979;hp=d2fc366cc77d88521d583558aa50d9680df9305e;hb=05f82cd6ab941db2d63ca83e778a430752de1900;hpb=663a0dcbf36fd68a8d5783fcf7b218d17e2f9aad

diff --git a/model.cc b/model.cc
index d2fc366c..508f3b98 100644
--- a/model.cc
+++ b/model.cc
@@ -1124,8 +1124,6 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
-			if (!act->is_write())
-				continue;
 			/* Reach synchronization -> this thread is complete */
 			if (act->happens_before(release))
 				break;
@@ -1134,6 +1132,10 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
 				continue;
 			}
 
+			/* Only writes can break release sequences */
+			if (!act->is_write())
+				continue;
+
 			/* Check modification order */
 			if (mo_graph->checkReachable(rf, act)) {
 				/* rf --mo--> act */