X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=da982d0db415395ed2be39e9dfcf3b34f74c1efe;hb=4ee9f33221f490599093e74b527ba7e401133f96;hp=1e730d794baca5dc99387053bb98125b3756193a;hpb=023c2e9d75b5f4460d1e079e4915b1c41a8045a4;p=model-checker.git

diff --git a/model.cc b/model.cc
index 1e730d7..da982d0 100644
--- a/model.cc
+++ b/model.cc
@@ -1388,7 +1388,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 {
 	std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
 	unsigned int i;
-
 	/* Iterate over all threads */
 	for (i = 0; i < thrd_lists->size(); i++) {
 		const ModelAction *write_after_read = NULL;
@@ -1403,7 +1402,7 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 				break;
 			else if (act->is_write())
 				write_after_read = act;
-			else if (act->is_read()&&act->get_reads_from()!=NULL) {
+			else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
 				write_after_read = act->get_reads_from();
 			}
 		}
@@ -1411,7 +1410,6 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 		if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
 			return false;
 	}
-
 	return true;
 }