diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 7f544b0ffd..a8ae198e14 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -23,8 +23,12 @@ struct let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg = let compute_refine_split (e:Mutexes.elt) = match e with | Addr a -> - let e' = BinOp(Eq, arg, AddrOf ((PreValueDomain.Mval.to_cil a)), intType) in - [Events.SplitBranch (e',true)] + let arg_e = AddrOf (PreValueDomain.Mval.to_cil a) in + if not (CilType.Exp.equal arg arg_e) then + let e' = BinOp(Eq, arg, AddrOf (PreValueDomain.Mval.to_cil a), intType) in + [Events.SplitBranch (e',true)] + else + [] | _ -> [] in match lv_opt with