From cf29a02731b7257e13cd9f666a920339fe581040 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 25 Sep 2012 16:39:07 -0700 Subject: [PATCH] model: bugfix - release sequences - handle Thread completion A completed Thread cannot generate any new writes that would break release sequences. --- model.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 66ca8be3..a9d94776 100644 --- a/model.cc +++ b/model.cc @@ -1161,7 +1161,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel bool future_ordered = false; ModelAction *last = get_last_action(int_to_id(i)); - if (last && rf->happens_before(last)) + if (last && (rf->happens_before(last) || + last->get_type() == THREAD_FINISH)) future_ordered = true; for (rit = list->rbegin(); rit != list->rend(); rit++) { -- 2.34.1