X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=fc2370616388d0c60acf8048fceee307e33ef269;hb=eb6e8431496fc3dfd7638fbfba4229f7215f6308;hp=33c862bac36fd2a7e788cfae00a1a46a774ecd4a;hpb=f9e2e3a893918a431d3af1e6657cd08260e31941;p=model-checker.git

diff --git a/execution.cc b/execution.cc
index 33c862b..fc23706 100644
--- a/execution.cc
+++ b/execution.cc
@@ -366,7 +366,10 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
 ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 {
 	switch (act->get_type()) {
-	/* case ATOMIC_FENCE: fences don't directly cause backtracking */
+	case ATOMIC_FENCE:
+		/* Only seq-cst fences can (directly) cause backtracking */
+		if (!act->is_seqcst())
+			break;
 	case ATOMIC_READ:
 	case ATOMIC_WRITE:
 	case ATOMIC_RMW: {
@@ -1209,7 +1212,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
  *
  * @param curr The current action to process
  * @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
  */
 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 {