model: fixup r_modification_order

Bugfix thanks to Brian D.

diff --git a/model.cc b/model.cc
index d8ae7ea4bf1eaa3c4ec2830d8c69f882ddb873c0..766e3694c32fffbff9240a836a3ed896e3b41103 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -652,7 +652,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
                         */
                        if (act->happens_before(curr) && act != curr) {
                                if (act->is_write()) {
                         */
                        if (act->happens_before(curr) && act != curr) {
                                if (act->is_write()) {

-                                       if (rf != act && act != curr) {
+                                       if (rf != act) {

                                                mo_graph->addEdge(act, rf);
                                                added = true;
                                        }
                                                mo_graph->addEdge(act, rf);
                                                added = true;
                                        }


@@ -663,7 +663,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
                                                added = true;
                                        }
                                }
                                                added = true;
                                        }
                                }

-

                                break;
                        }
                }
                                break;
                        }
                }