X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;fp=execution.cc;h=01a5fa442b0905b522f05714d95dc7eaf5fa56a2;hp=3a630d777f060cb22598858278044d6e140cfed3;hb=3fe3c730dd6a8deb536276f7a68ef58cae0d74f3;hpb=6014243b7130f34b7ffd1098da225b0b8de5c328 diff --git a/execution.cc b/execution.cc index 3a630d7..01a5fa4 100644 --- a/execution.cc +++ b/execution.cc @@ -1753,9 +1753,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) - continue; - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + if (act->get_reads_from() == NULL) { + added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; + } else + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) &&