diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 34b4289f7..dd5fed01a 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -41,11 +41,18 @@ let join astate1 astate2 = then astate1 else IdMap.merge - (fun _ ap1_opt ap2_opt -> match ap1_opt, ap2_opt with + (fun var ap1_opt ap2_opt -> match ap1_opt, ap2_opt with | Some ap1, Some ap2 -> (* in principle, could do a join here if the access paths have the same root. but they should always be equal if we are using the map correctly *) - assert (AccessPath.raw_equal ap1 ap2); + let check_invariant () = match var with + | Var.ProgramVar pvar when Pvar.is_frontend_tmp pvar -> + (* Sawja reuses temporary variables which sometimes breaks this invariant *) + (* TODO: fix (13370224) *) + () + | _ -> + assert (AccessPath.raw_equal ap1 ap2) in + check_invariant (); ap1_opt | Some _, None -> ap1_opt | None, Some _ -> ap2_opt