From 91d0f5816b8c131bd3842b16bec7bdf174f46b83 Mon Sep 17 00:00:00 2001
From: Gaurav Parthasarathy <gauravp@student.ethz.ch>
Date: Thu, 11 Jul 2019 00:22:48 +0200
Subject: [PATCH] adjusted proph_extract_winner to only consider the thread
identifier
---
theories/logatom/rdcss/rdcss.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 3e3eaea6..233fd939 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -163,7 +163,7 @@ Section rdcss.
Fixpoint proph_extract_winner (pvs : list (val * val)) : option proph_id :=
match pvs with
- | ((_, #true)%V, LitV (LitProphecy tid)) :: _ => Some tid
+ | ((_, _)%V, LitV (LitProphecy tid)) :: _ => Some tid
| _ => None
end.
--
GitLab