diff --git a/infer/src/IR/Struct.ml b/infer/src/IR/Struct.ml
index 078914a16..b11163af1 100644
--- a/infer/src/IR/Struct.ml
+++ b/infer/src/IR/Struct.ml
@@ -272,3 +272,10 @@ let merge typename ~newer ~current =
       newer
   | JavaClass _ ->
       full_merge ~newer ~current
+
+
+let is_not_java_interface = function
+  | {java_class_info= Some {kind= Interface}} ->
+      false
+  | _ ->
+      true
diff --git a/infer/src/IR/Struct.mli b/infer/src/IR/Struct.mli
index 707356322..469089115 100644
--- a/infer/src/IR/Struct.mli
+++ b/infer/src/IR/Struct.mli
@@ -75,3 +75,7 @@ val add_sub : Typ.Name.t -> t -> t
 
 val merge : Typ.Name.t -> newer:t -> current:t -> t
 (** best effort directed merge of two structs for the same typename *)
+
+val is_not_java_interface : t -> bool
+(** check that a struct either defines a non-java type, or a non-java-interface type (abstract or
+    normal class) *)
diff --git a/infer/src/IR/Tenv.ml b/infer/src/IR/Tenv.ml
index 57bea058a..5b3e599d2 100644
--- a/infer/src/IR/Tenv.ml
+++ b/infer/src/IR/Tenv.ml
@@ -243,3 +243,37 @@ let get_summary_formals tenv ~get_summary ~get_formals =
             `NotFound ) )
   in
   fun pname -> get_summary_formals_aux pname
+
+
+let resolve_method ~method_exists tenv class_name proc_name =
+  let visited = ref Typ.Name.Set.empty in
+  let rec resolve_name_struct (class_name : Typ.Name.t) (class_struct : Struct.t) =
+    if
+      (not (Typ.Name.is_class class_name))
+      || (not (Struct.is_not_java_interface class_struct))
+      || Typ.Name.Set.mem class_name !visited
+    then None
+    else (
+      visited := Typ.Name.Set.add class_name !visited ;
+      let right_proc_name = Procname.replace_class proc_name class_name in
+      if method_exists right_proc_name class_struct.methods then Some right_proc_name
+      else
+        let supers_to_search =
+          match (class_name : Typ.Name.t) with
+          | CStruct _ | CUnion _ | CppClass _ ->
+              (* multiple inheritance possible, search all supers *)
+              class_struct.supers
+          | JavaClass _ ->
+              (* multiple inheritance not possible, but cannot distinguish interfaces from typename so search all *)
+              class_struct.supers
+          | ObjcClass _ ->
+              (* multiple inheritance impossible, but recursive calls will throw away protocols *)
+              class_struct.supers
+          | ObjcProtocol _ ->
+              []
+        in
+        List.find_map supers_to_search ~f:resolve_name )
+  and resolve_name class_name =
+    lookup tenv class_name |> Option.bind ~f:(resolve_name_struct class_name)
+  in
+  resolve_name class_name
diff --git a/infer/src/IR/Tenv.mli b/infer/src/IR/Tenv.mli
index 8b4e4fd86..539da76a5 100644
--- a/infer/src/IR/Tenv.mli
+++ b/infer/src/IR/Tenv.mli
@@ -65,6 +65,17 @@ val merge_per_file : src:per_file -> dst:per_file -> per_file
 (** Best-effort merge of [src] into [dst]. If a procedure is both in [dst] and [src], the one in
     [dst] will get overwritten. *)
 
+val resolve_method :
+     method_exists:(Procname.t -> Procname.t list -> bool)
+  -> t
+  -> Typ.Name.t
+  -> Procname.t
+  -> Procname.t option
+(** [resolve_method ~method_exists tenv class_name procname] tries to resolve [procname] to a method
+    in [class_name] or its super-classes, that is non-virtual (non-Java-interface method).
+    [method_exists adapted_procname methods] should check if [adapted_procname] ([procname] but with
+    its class potentially changed to some [other_class]) is among the [methods] of [other_class]. *)
+
 val get_summary_formals :
      t
   -> get_summary:(Procname.t -> 'summary option)
diff --git a/infer/src/backend/Devirtualizer.ml b/infer/src/backend/Devirtualizer.ml
index 5f8a929bf..c16ded845 100644
--- a/infer/src/backend/Devirtualizer.ml
+++ b/infer/src/backend/Devirtualizer.ml
@@ -99,16 +99,7 @@ let analyze_at_node (map : Analyzer.invariant_map) node : Domain.t =
 (* inspired from biabduction/Symexec.ml, function resolve_method  *)
 let resolve_method tenv class_name proc_name =
   let method_exists pname methods = List.exists ~f:(Procname.equal pname) methods in
-  let rec resolve class_name =
-    let resolved_proc_name = Procname.replace_class proc_name class_name in
-    match Tenv.lookup tenv class_name with
-    | Some {methods; supers} when Typ.Name.is_class class_name -> (
-        if method_exists resolved_proc_name methods then Some resolved_proc_name
-        else match supers with super_classname :: _ -> resolve super_classname | _ -> None )
-    | _ ->
-        None
-  in
-  resolve class_name
+  Tenv.resolve_method ~method_exists tenv class_name proc_name
 
 
 let process summary tenv =
diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml
index 4a04b236a..0f0d87727 100644
--- a/infer/src/biabduction/SymExec.ml
+++ b/infer/src/biabduction/SymExec.ml
@@ -431,27 +431,7 @@ let method_exists right_proc_name methods =
 
 
 let resolve_method tenv class_name proc_name =
-  let found_class =
-    let visited = ref Typ.Name.Set.empty in
-    let rec resolve (class_name : Typ.Name.t) =
-      visited := Typ.Name.Set.add class_name !visited ;
-      let right_proc_name = Procname.replace_class proc_name class_name in
-      match Tenv.lookup tenv class_name with
-      | Some {methods; supers} when Typ.Name.is_class class_name -> (
-          if method_exists right_proc_name methods then Some right_proc_name
-          else
-            match supers with
-            | super_classname :: _ ->
-                if not (Typ.Name.Set.mem super_classname !visited) then resolve super_classname
-                else None
-            | _ ->
-                None )
-      | _ ->
-          None
-    in
-    resolve class_name
-  in
-  match found_class with
+  match Tenv.resolve_method ~method_exists tenv class_name proc_name with
   | None ->
       Logging.d_printfln "Couldn't find method in the hierarchy of type %s"
         (Typ.Name.name class_name) ;