model: add release sequence model_thread ASSERT()

This ASSERT() should ensure that model-checker threads are always
'future_ordered'.

diff --git a/model.cc b/model.cc
index 1fcb8fc0a2ab34b375d7c905e0f32c81699afef8..8e3af8a37c13836ac466055ed039ebeea9cbf6b3 100644 (file)
--- 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 */