From 04980c8b06eb8f1688876dd0989c64e4bc8bcb5b Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Sun, 7 Oct 2012 15:23:37 -0700
Subject: [PATCH] model: add release sequence model_thread ASSERT()

This ASSERT() should ensure that model-checker threads are always
'future_ordered'.
---
 model.cc | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/model.cc b/model.cc
index 1fcb8fc..8e3af8a 100644
--- a/model.cc
+++ b/model.cc
@@ -1334,6 +1334,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 				th->is_complete())
 			future_ordered = true;
 
+		ASSERT(!th->is_model_thread() || future_ordered);
+
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			const ModelAction *act = *rit;
 			/* Reach synchronization -> this thread is complete */
-- 
2.34.1