X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=action.cc;fp=action.cc;h=d4c6253caf20c23411c60ba350a91760c386e6fc;hp=876de1262c82475f3f9e6610ba339f305963a0a5;hb=178fa56c36e45267d59c545dea0b9c7be93a4e1e;hpb=3897cb4ac31fe710f2333bd6ca917144b58844f2 diff --git a/action.cc b/action.cc index 876de12..d4c6253 100644 --- a/action.cc +++ b/action.cc @@ -330,7 +330,7 @@ bool ModelAction::could_synchronize_with(const ModelAction *act) const return false; // Different locations commute - if (!same_var(act)) + if (!same_var(act) && !is_fence() && !act->is_fence()) return false; // Explore interleavings of seqcst writes/fences to guarantee total