- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (act==reader)
- break;
- if (act->is_write())
- first_write_after_read=act;
+ if (!reader->happens_before(act))
+ break;
+ else if (act->is_write())
+ write_after_read = act;
+ else if (act->is_read()&&act->get_reads_from()!=NULL&&act!=reader) {
+ write_after_read = act->get_reads_from();
+ }
+ }
+
+ if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
+ return false;