X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=9aaab916849f466d66578d42108e55c1567ba41f;hb=3eb987279c382e0000de844728aceef2f360acf6;hp=c707ff8771b023d0f4b71b259e42dce77b7105e6;hpb=75fd45bf45d7ec1ac8db7cb6209106ea4e3fc5ab;p=model-checker.git diff --git a/model.cc b/model.cc index c707ff8..9aaab91 100644 --- a/model.cc +++ b/model.cc @@ -2475,7 +2475,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, } // Don't do any lookups twice for the same thread - if (promise->thread_is_eliminated(tid)) + if (!promise->thread_is_available(tid)) continue; if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {