From 1b4beae60e768f729843a600d387d5bd00fe0911 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 25 Dec 2024 20:01:08 +0100 Subject: [PATCH] Get rid of overcomplicated logic --- src/analyses/pthreadBarriers.ml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml index 83e253f66f..4ea5f1540a 100644 --- a/src/analyses/pthreadBarriers.ml +++ b/src/analyses/pthreadBarriers.ml @@ -79,13 +79,6 @@ struct let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in if Z.leq min_cap Z.one then true, must - else if min_cap = Z.of_int 2 && count = 1 then - let elem = Waiters.choose relevant_waiters in - let curr = MustObserved.find (MHPplusLock.tid elem) must in - let must' = MustObserved.add (MHPplusLock.tid elem) (Barriers.add addr curr) must in - true, must' - else if min_cap = Z.of_int 2 && count >= 1 then - true, must else if Z.geq (Z.of_int (count + 1)) min_cap then (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that MHP is pairwise true? This solution is a sledgehammer, there should be something much