diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
index ed6bc73ff04..3cbf89e37a1 100644
--- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp
+++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp
@@ -59,6 +59,7 @@ require_goto_statements::require_entry_point_statements(
 /// \param structure_name: The name of variable of type struct
 /// \param superclass_name: The name of the superclass (if given)
 /// \param component_name: The name of the component of the superclass that
+/// \param symbol_table: A symbol table to enable type lookups
 /// should be assigned
 /// \return: All the assignments to that component.
 require_goto_statements::pointer_assignment_locationt
@@ -66,7 +67,8 @@ require_goto_statements::find_struct_component_assignments(
   const std::vector<codet> &statements,
   const irep_idt &structure_name,
   const optionalt<irep_idt> &superclass_name,
-  const irep_idt &component_name)
+  const irep_idt &component_name,
+  const symbol_tablet &symbol_table)
 {
   pointer_assignment_locationt locations;
 
@@ -97,9 +99,13 @@ require_goto_statements::find_struct_component_assignments(
             const irep_idt supercomponent_name =
               "@" + id2string(superclass_name.value());
 
+            object_descriptor_exprt ode;
+            const namespacet ns(symbol_table);
+            ode.build(superclass_expr, ns);
             if(
               superclass_expr.get_component_name() == supercomponent_name &&
-              superclass_expr.symbol().get_identifier() == structure_name)
+              to_symbol_expr(ode.root_object()).get_identifier() ==
+              structure_name)
             {
               if(
                 code_assign.rhs() ==
@@ -122,7 +128,7 @@ require_goto_statements::find_struct_component_assignments(
           // - operand (component of): symbol for \p structure_name
           if(
             member_expr.op().id() == ID_symbol &&
-            member_expr.symbol().get_identifier() == structure_name &&
+            to_symbol_expr(member_expr.op()).get_identifier() == structure_name &&
             member_expr.get_component_name() == component_name)
           {
             if(
@@ -291,6 +297,7 @@ const code_declt &require_goto_statements::require_declaration_of_name(
 /// \param typecast_name The name of the type to which the object is cast (if
 /// there is a typecast)
 /// \param entry_point_instructions The statements to look through
+/// \param symbol_table: A symbol table to enable type lookups
 /// \return The identifier of the variable assigned to the field
 const irep_idt &require_goto_statements::require_struct_component_assignment(
   const irep_idt &structure_name,
@@ -298,7 +305,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
   const irep_idt &component_name,
   const irep_idt &component_type_name,
   const optionalt<irep_idt> &typecast_name,
-  const std::vector<codet> &entry_point_instructions)
+  const std::vector<codet> &entry_point_instructions,
+  const symbol_tablet &symbol_table)
 {
   // First we need to find the assignments to the component belonging to
   // the structure_name object
@@ -307,7 +315,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
       entry_point_instructions,
       structure_name,
       superclass_name,
-      component_name);
+      component_name,
+      symbol_table);
   REQUIRE(component_assignments.non_null_assignments.size() == 1);
 
   // We are expecting that the resulting statement can be of two forms:
@@ -376,6 +385,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
 /// \param array_type_name The type of the array, e.g., java::array[reference]
 /// \param array_component_element_type_name The element type of the array
 /// \param entry_point_instructions The statements to look through
+/// \param symbol_table: A symbol table to enable type lookups
 /// \return The identifier of the variable assigned to the field
 const irep_idt &
 require_goto_statements::require_struct_array_component_assignment(
@@ -384,7 +394,8 @@ require_goto_statements::require_struct_array_component_assignment(
   const irep_idt &array_component_name,
   const irep_idt &array_type_name,
   const irep_idt &array_component_element_type_name,
-  const std::vector<codet> &entry_point_instructions)
+  const std::vector<codet> &entry_point_instructions,
+  const symbol_tablet &symbol_table)
 {
   // First we need to find the assignments to the component belonging to
   // the structure_name object
@@ -393,7 +404,8 @@ require_goto_statements::require_struct_array_component_assignment(
       entry_point_instructions,
       structure_name,
       superclass_name,
-      array_component_name);
+      array_component_name,
+      symbol_table);
   REQUIRE(component_assignments.non_null_assignments.size() == 1);
 
   // We are expecting that the resulting statement is of form:
diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h
index 7feb210a7ff..d22ad9d315c 100644
--- a/jbmc/unit/java-testing-utils/require_goto_statements.h
+++ b/jbmc/unit/java-testing-utils/require_goto_statements.h
@@ -53,7 +53,8 @@ pointer_assignment_locationt find_struct_component_assignments(
   const std::vector<codet> &statements,
   const irep_idt &structure_name,
   const optionalt<irep_idt> &superclass_name,
-  const irep_idt &component_name);
+  const irep_idt &component_name,
+  const symbol_tablet &symbol_table);
 
 pointer_assignment_locationt find_this_component_assignment(
   const std::vector<codet> &statements,
@@ -82,7 +83,8 @@ const irep_idt &require_struct_component_assignment(
   const irep_idt &component_name,
   const irep_idt &component_type_name,
   const optionalt<irep_idt> &typecast_name,
-  const std::vector<codet> &entry_point_instructions);
+  const std::vector<codet> &entry_point_instructions,
+  const symbol_tablet &symbol_table);
 
 const irep_idt &require_struct_array_component_assignment(
   const irep_idt &structure_name,
@@ -90,7 +92,8 @@ const irep_idt &require_struct_array_component_assignment(
   const irep_idt &array_component_name,
   const irep_idt &array_type_name,
   const irep_idt &array_component_element_type_name,
-  const std::vector<codet> &entry_point_instructions);
+  const std::vector<codet> &entry_point_instructions,
+  const symbol_tablet &symbol_table);
 
 const irep_idt &require_entry_point_argument_assignment(
   const irep_idt &argument_name,
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
index 472e119494d..8d264669736 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp
@@ -58,7 +58,8 @@ SCENARIO(
           "field",
           "java::java.lang.Integer",
           {"java::java.lang.Object"},
-          entry_point_code);
+          entry_point_code,
+          symbol_table);
       }
     }
   }
@@ -90,7 +91,8 @@ SCENARIO(
           "field",
           "java::IWrapper",
           {"java::java.lang.Object"},
-          entry_point_code);
+          entry_point_code,
+          symbol_table);
       }
     }
   }
@@ -122,7 +124,8 @@ SCENARIO(
             "field",
             "java::Wrapper",
             {"java::java.lang.Object"},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'this.field' has correctly specialized field")
         {
@@ -132,7 +135,8 @@ SCENARIO(
             "field",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -167,7 +171,8 @@ SCENARIO(
             "f",
             "java::SuperclassUninst",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("The object for 'f' has correctly specialized inherited field")
         {
@@ -177,7 +182,8 @@ SCENARIO(
             "field",
             "java::java.lang.Integer",
             {"java::java.lang.Object"},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -210,7 +216,8 @@ SCENARIO(
             "f",
             "java::SuperclassMixed",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("The object for 'f' has correctly specialized inherited fields")
         {
@@ -220,7 +227,8 @@ SCENARIO(
             "first",
             "java::java.lang.Boolean",
             {"java::java.lang.Object"},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
           require_goto_statements::require_struct_component_assignment(
             f_tmp_name,
@@ -228,7 +236,8 @@ SCENARIO(
             "second",
             "java::IWrapper",
             {"java::java.lang.Object"},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -265,7 +274,8 @@ SCENARIO(
             "inner",
             "java::SuperclassInnerInst$Inner",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         THEN(
           "The object of 'inner' has correctly specialized inherited "
           "field")
@@ -276,7 +286,8 @@ SCENARIO(
             "field",
             "java::java.lang.Integer",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
 
         const irep_idt &inner_gen_tmp_name =
@@ -286,7 +297,8 @@ SCENARIO(
             "inner_gen",
             "java::SuperclassInnerInst$InnerGen",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         THEN(
           "The object of 'inner_gen' has correctly specialized inherited "
           "field")
@@ -297,7 +309,8 @@ SCENARIO(
             "field",
             "java::java.lang.Boolean",
             {"java::java.lang.Object"},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -334,7 +347,8 @@ SCENARIO(
             "f",
             "java::SuperclassInnerUninst",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN(
           "The object for 'f' has fields 'inner' and 'inner_gen' "
@@ -347,7 +361,8 @@ SCENARIO(
               "inner",
               "java::SuperclassInnerUninst$Inner",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           THEN(
             "The object of 'inner' has correctly specialized inherited "
             "field")
@@ -358,7 +373,8 @@ SCENARIO(
               "field",
               "java::IWrapper",
               {"java::java.lang.Object"},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           }
 
           const irep_idt &inner_gen_tmp_name =
@@ -368,7 +384,8 @@ SCENARIO(
               "inner_gen",
               "java::SuperclassInnerUninst$InnerGen",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           THEN(
             "The object of 'inner_gen' has correctly specialized inherited "
             "fields")
@@ -379,14 +396,16 @@ SCENARIO(
               "first",
               "java::IWrapper",
               {"java::java.lang.Object"},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
             require_goto_statements::require_struct_component_assignment(
               inner_gen_tmp_name,
               {"PairWrapper"},
               "second",
               "java::java.lang.Boolean",
               {"java::java.lang.Object"},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           }
 
           const irep_idt &inner_three_tmp_name =
@@ -396,7 +415,8 @@ SCENARIO(
               "inner_three",
               "java::SuperclassInnerUninst$InnerThree",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           THEN(
             "The object of 'inner_three' has correctly specialized "
             "inherited fields")
@@ -407,7 +427,8 @@ SCENARIO(
               "field",
               "java::IWrapper",
               {"java::java.lang.Object"},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           }
         }
       }
@@ -463,7 +484,8 @@ SCENARIO(
           "field",
           "java::java.lang.Object",
           {},
-          entry_point_code);
+          entry_point_code,
+          symbol_table);
       }
     }
   }
@@ -506,7 +528,8 @@ SCENARIO(
           "field",
           "java::java.lang.Object",
           {},
-          entry_point_code);
+          entry_point_code,
+          symbol_table);
       }
     }
   }
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
index c80824631c6..660d15576be 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp
@@ -50,7 +50,8 @@ SCENARIO(
             "field_input",
             "java::Wrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'field_input' has field 'field' of type IWrapper")
         {
@@ -60,7 +61,8 @@ SCENARIO(
             "field",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
         THEN("Object 'field_input' has field 'array_field' of type IWrapper[]")
         {
@@ -70,7 +72,8 @@ SCENARIO(
             "array_field",
             "java::array[reference]",
             "java::IWrapper",
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -126,7 +129,8 @@ SCENARIO(
             "field_input1",
             "java::Wrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'field_input1' has field 'field' of type IWrapper")
         {
@@ -136,7 +140,8 @@ SCENARIO(
             "field",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
 
@@ -149,7 +154,8 @@ SCENARIO(
             "field_input2",
             "java::Wrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'field_input2' has field 'field' of type BWrapper")
         {
@@ -159,7 +165,8 @@ SCENARIO(
             "field",
             "java::BWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -193,7 +200,8 @@ SCENARIO(
             "field_input1",
             "java::Wrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'field_input1' has field 'field' of type Wrapper")
         {
@@ -204,12 +212,19 @@ SCENARIO(
               "field",
               "java::Wrapper",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
 
           THEN("Object 'field' has field 'field' of type IWrapper")
           {
             require_goto_statements::require_struct_component_assignment(
-              field_name, {}, "field", "java::IWrapper", {}, entry_point_code);
+              field_name,
+              {},
+              "field",
+              "java::IWrapper",
+              {},
+              entry_point_code,
+              symbol_table);
           }
         }
       }
@@ -243,7 +258,8 @@ SCENARIO(
             "field_input",
             "java::PairWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'field_input' has field 'key' of type IWrapper")
         {
@@ -253,7 +269,8 @@ SCENARIO(
             "first",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
 
         THEN("Object 'field_input' has field 'value' of type IWrapper")
@@ -264,7 +281,8 @@ SCENARIO(
             "second",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -311,7 +329,8 @@ SCENARIO(
             "field",
             "java::IWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -362,7 +381,8 @@ SCENARIO(
             "field",
             "java::java.lang.Object",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -412,7 +432,8 @@ SCENARIO(
               "field",
               "java::GenericFields$GenericInnerOuter$Outer$InnerClass",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
 
           THEN("Object 'field' has field 't' of type Integer")
           {
@@ -422,7 +443,8 @@ SCENARIO(
               "t",
               "java::java.lang.Integer",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           }
         }
       }
@@ -474,7 +496,8 @@ SCENARIO(
             "value",
             "java::java.lang.Integer",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
 
         THEN("Object 'v' has field 'field' of type A")
@@ -486,7 +509,8 @@ SCENARIO(
               "field",
               "java::GenericFields$GenericRewriteParameter$A",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
 
           THEN("Object 'field' has field 'value' of type Boolean")
           {
@@ -496,7 +520,8 @@ SCENARIO(
               "value",
               "java::java.lang.Boolean",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           }
         }
       }
@@ -554,7 +579,8 @@ SCENARIO(
             "f",
             "java::UnsupportedWrapper2",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'f' has unspecialized field 'field'")
         {
@@ -567,7 +593,8 @@ SCENARIO(
             "field",
             "java::java.lang.Object",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
@@ -612,7 +639,8 @@ SCENARIO(
             "f",
             "java::OpaqueWrapper",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
 
         THEN("Object 'f' has unspecialized field 'field'")
         {
@@ -622,7 +650,8 @@ SCENARIO(
             "field",
             "java::java.lang.Object",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         }
       }
     }
diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
index 296e2ffaf11..6044b5596db 100644
--- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
+++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp
@@ -91,9 +91,9 @@ SCENARIO(
       const irep_idt &key_type,
       const irep_idt &val_type) {
       require_goto_statements::require_struct_component_assignment(
-        field, {}, "key", key_type, {}, entry_point_code);
+        field, {}, "key", key_type, {}, entry_point_code, symbol_table);
       require_goto_statements::require_struct_component_assignment(
-        field, {}, "value", val_type, {}, entry_point_code);
+        field, {}, "value", val_type, {}, entry_point_code, symbol_table);
     };
 
     const irep_idt &tmp_object_name =
@@ -110,7 +110,8 @@ SCENARIO(
           "example1",
           "java::KeyValue",
           {},
-          entry_point_code);
+          entry_point_code,
+          symbol_table);
 
       THEN(
         "Object 'example1' has field 'key' of type `String` and field `value` "
@@ -124,7 +125,13 @@ SCENARIO(
       {
         const auto &next_field =
           require_goto_statements::require_struct_component_assignment(
-            example1_field, {}, "next", "java::KeyValue", {}, entry_point_code);
+            example1_field,
+            {},
+            "next",
+            "java::KeyValue",
+            {},
+            entry_point_code,
+            symbol_table);
         has_key_and_value_field(
           next_field, "java::java.lang.String", "java::java.lang.Integer");
       }
@@ -137,7 +144,8 @@ SCENARIO(
             "reverse",
             "java::KeyValue",
             {},
-            entry_point_code);
+            entry_point_code,
+            symbol_table);
         has_key_and_value_field(
           reverse_field, "java::java.lang.Integer", "java::java.lang.String");
       }
@@ -148,7 +156,13 @@ SCENARIO(
     {
       const auto &example2_field =
         require_goto_statements::require_struct_component_assignment(
-          tmp_object_name, {}, "example2", "java::Three", {}, entry_point_code);
+          tmp_object_name,
+          {},
+          "example2",
+          "java::Three",
+          {},
+          entry_point_code,
+          symbol_table);
 
       const auto has_x_e_u_fields = [&](
         const irep_idt &field,
@@ -156,11 +170,11 @@ SCENARIO(
         const irep_idt &e_type,
         const irep_idt &u_type) {
         require_goto_statements::require_struct_component_assignment(
-          field, {}, "x", x_type, {}, entry_point_code);
+          field, {}, "x", x_type, {}, entry_point_code, symbol_table);
         require_goto_statements::require_struct_component_assignment(
-          field, {}, "e", e_type, {}, entry_point_code);
+          field, {}, "e", e_type, {}, entry_point_code, symbol_table);
         require_goto_statements::require_struct_component_assignment(
-          field, {}, "u", u_type, {}, entry_point_code);
+          field, {}, "u", u_type, {}, entry_point_code, symbol_table);
       };
 
       THEN(
@@ -182,7 +196,8 @@ SCENARIO(
               "rotate",
               "java::Three",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           has_x_e_u_fields(
             rotate_field,
             "java::java.lang.Integer",
@@ -198,7 +213,8 @@ SCENARIO(
                 "rotate",
                 "java::Three",
                 {},
-                entry_point_code);
+                entry_point_code,
+                symbol_table);
             has_x_e_u_fields(
               rotate_rec_field,
               "java::java.lang.Character",
@@ -214,7 +230,8 @@ SCENARIO(
                 "normal",
                 "java::Three",
                 {},
-                entry_point_code);
+                entry_point_code,
+                symbol_table);
             has_x_e_u_fields(
               rotate_normal_field,
               "java::java.lang.Integer",
@@ -231,7 +248,8 @@ SCENARIO(
               "normal",
               "java::Three",
               {},
-              entry_point_code);
+              entry_point_code,
+              symbol_table);
           has_x_e_u_fields(
             normal_field,
             "java::java.lang.Byte",
@@ -246,7 +264,8 @@ SCENARIO(
                 "normal",
                 "java::Three",
                 {},
-                entry_point_code);
+                entry_point_code,
+                symbol_table);
             has_x_e_u_fields(
               normal_rec_field,
               "java::java.lang.Byte",
@@ -262,7 +281,8 @@ SCENARIO(
                 "rotate",
                 "java::Three",
                 {},
-                entry_point_code);
+                entry_point_code,
+                symbol_table);
             has_x_e_u_fields(
               normal_rotate_field,
               "java::java.lang.Integer",
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 1b3b78eb085..85ca4a6b3a2 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -3529,18 +3529,6 @@ class member_exprt:public unary_exprt
   {
     return op0();
   }
-
-  // Retrieves the object(symbol) this member corresponds to
-  inline const symbol_exprt &symbol() const
-  {
-    const exprt &op=op0();
-    if(op.id()==ID_member)
-    {
-      return static_cast<const member_exprt &>(op).symbol();
-    }
-
-    return to_symbol_expr(op);
-  }
 };
 
 /// \brief Cast an exprt to a \ref member_exprt