diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index 86c181374af..f0fcb99b189 100644
--- a/src/analyses/ai.cpp
+++ b/src/analyses/ai.cpp
@@ -462,7 +462,7 @@ bool ai_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index 42a110e42a4..ce55e807979 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -293,7 +293,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     if(recursion_set.find(identifier)!=recursion_set.end())
     {
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index bd83043140e..8c4afe661b4 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -143,7 +143,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   }
 
   if(expr.id()==ID_symbol)
-    return expr.get_string(ID_identifier);
+    return id2string(to_symbol_expr(expr).get_identifier());
 
   return "";
 }
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
index 0ee8ef3841b..32504c7c4e1 100644
--- a/src/analyses/static_analysis.cpp
+++ b/src/analyses/static_analysis.cpp
@@ -328,7 +328,7 @@ void static_analysis_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     if(recursion_set.find(identifier)!=recursion_set.end())
     {
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index 9d51bca80e8..4e0d2d31d0c 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -262,8 +262,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 
   while(result_type.id()==ID_symbol)
   {
-    const symbolt &followed_type_symbol=
-      ns.lookup(result_type.get(ID_identifier));
+    const symbolt &followed_type_symbol =
+      ns.lookup(to_symbol_type(result_type));
 
     result_type=followed_type_symbol.type;
     qualifiers+=c_qualifierst(followed_type_symbol.type);
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index 614b46b7ea0..b17d92752fe 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 
@@ -180,7 +181,7 @@ static std::string type2name(
     const array_typet &t=to_array_type(type);
     mp_integer size;
     if(t.size().id()==ID_symbol)
-      result+="ARR"+id2string(t.size().get(ID_identifier));
+      result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
     else if(to_integer(t.size(), size))
       result+="ARR?";
     else
diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp
index 5cd698fd718..5ea145f505f 100644
--- a/src/cpp/cpp_is_pod.cpp
+++ b/src/cpp/cpp_is_pod.cpp
@@ -82,8 +82,8 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const
   }
   else if(type.id()==ID_symbol)
   {
-    const symbolt &symb=lookup(type.get(ID_identifier));
-    assert(symb.is_type);
+    const symbolt &symb = lookup(to_symbol_type(type));
+    DATA_INVARIANT(symb.is_type, "type symbol is a type");
     return cpp_is_pod(symb.type);
   }
 
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 3eca6b3bc12..3a74207a96e 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -170,9 +170,9 @@ void cpp_typecheck_resolvet::remove_duplicates(
     irep_idt id;
 
     if(it->id()==ID_symbol)
-      id=it->get(ID_identifier);
+      id = to_symbol_expr(*it).get_identifier();
     else if(it->id()==ID_type && it->type().id()==ID_symbol)
-      id=it->type().get(ID_identifier);
+      id = to_symbol_type(it->type()).get_identifier();
 
     if(id=="")
     {
@@ -2041,8 +2041,8 @@ void cpp_typecheck_resolvet::apply_template_args(
   if(expr.id()!=ID_symbol)
     return; // templates are always symbols
 
-  const symbolt &template_symbol=
-    cpp_typecheck.lookup(expr.get(ID_identifier));
+  const symbolt &template_symbol =
+    cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
 
   if(!template_symbol.type.get_bool(ID_is_template))
     return;
@@ -2239,7 +2239,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
         const typet &type=pcomp.type();
         assert(type.id()!=ID_struct);
         if(type.id()==ID_symbol)
-          identifier=type.get(ID_identifier);
+          identifier = to_symbol_type(type).get_identifier();
         else
           continue;
       }
@@ -2261,7 +2261,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           break;
         }
         else if(symbol.type.id()==ID_symbol)
-          identifier=symbol.type.get(ID_identifier);
+          identifier = to_symbol_type(symbol.type).get_identifier();
         else
           break;
       }
diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp
index 3526603d1dc..02d901e391f 100644
--- a/src/cpp/template_map.cpp
+++ b/src/cpp/template_map.cpp
@@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <ostream>
 
 #include <util/invariant.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 void template_mapt::apply(typet &type) const
 {
@@ -39,8 +41,8 @@ void template_mapt::apply(typet &type) const
   }
   else if(type.id()==ID_symbol)
   {
-    type_mapt::const_iterator m_it=
-      type_map.find(type.get(ID_identifier));
+    type_mapt::const_iterator m_it =
+      type_map.find(to_symbol_type(type).get_identifier());
 
     if(m_it!=type_map.end())
     {
@@ -73,8 +75,8 @@ void template_mapt::apply(exprt &expr) const
 
   if(expr.id()==ID_symbol)
   {
-    expr_mapt::const_iterator m_it=
-      expr_map.find(expr.get(ID_identifier));
+    expr_mapt::const_iterator m_it =
+      expr_map.find(to_symbol_expr(expr).get_identifier());
 
     if(m_it!=expr_map.end())
     {
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index de4f0001113..52c3cf2650c 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -29,11 +29,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void goto_convertt::do_prob_uniform(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &identifier=function.get(ID_identifier);
+  const irep_idt &identifier = function.get_identifier();
 
   // make it a side effect if there is an LHS
   if(arguments.size()!=2)
@@ -107,11 +107,11 @@ void goto_convertt::do_prob_uniform(
 
 void goto_convertt::do_prob_coin(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &identifier=function.get(ID_identifier);
+  const irep_idt &identifier = function.get_identifier();
 
   // make it a side effect if there is an LHS
   if(arguments.size()!=2)
@@ -184,11 +184,11 @@ void goto_convertt::do_prob_coin(
 
 void goto_convertt::do_printf(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &f_id=function.get(ID_identifier);
+  const irep_idt &f_id = function.get_identifier();
 
   if(f_id==CPROVER_PREFIX "printf" ||
      f_id=="printf")
@@ -219,11 +219,11 @@ void goto_convertt::do_printf(
 
 void goto_convertt::do_scanf(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &f_id=function.get(ID_identifier);
+  const irep_idt &f_id = function.get_identifier();
 
   if(f_id==CPROVER_PREFIX "scanf")
   {
@@ -364,7 +364,7 @@ void goto_convertt::do_output(
 
 void goto_convertt::do_atomic_begin(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
@@ -388,7 +388,7 @@ void goto_convertt::do_atomic_begin(
 
 void goto_convertt::do_atomic_end(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
@@ -597,7 +597,7 @@ exprt goto_convertt::get_array_argument(const exprt &src)
 void goto_convertt::do_array_op(
   const irep_idt &id,
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index f775b61deea..717ec40085e 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -657,16 +657,16 @@ void goto_convertt::convert_decl(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  const exprt &op0=code.op0();
+  const exprt &op = code.symbol();
 
-  if(op0.id()!=ID_symbol)
+  if(op.id() != ID_symbol)
   {
-    error().source_location=op0.find_source_location();
-    error() << "decl statement expects symbol as first operand" << eom;
+    error().source_location = op.find_source_location();
+    error() << "decl statement expects symbol as operand" << eom;
     throw 0;
   }
 
-  const irep_idt &identifier=op0.get(ID_identifier);
+  const irep_idt &identifier = to_symbol_expr(op).get_identifier();
 
   const symbolt &symbol = ns.lookup(identifier);
 
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index a728dbf712c..273bf099da9 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -606,38 +606,38 @@ class goto_convertt:public messaget
   // some built-in functions
   void do_atomic_begin(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_atomic_end(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_create_thread(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_array_equal(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_array_op(
     const irep_idt &id,
     const exprt &lhs,
-    const exprt &function,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_printf(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_scanf(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_input(
@@ -652,12 +652,12 @@ class goto_convertt:public messaget
     goto_programt &dest);
   void do_prob_coin(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_prob_uniform(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
 
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index a4db2365e2c..7a73da9629f 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -373,7 +373,7 @@ void goto_convertt::remove_function_call(
 
   if(expr.op0().id()==ID_symbol)
   {
-    const irep_idt &identifier=expr.op0().get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(expr.op0()).get_identifier();
     const symbolt &symbol = ns.lookup(identifier);
 
     new_base_name+='_';
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 1b24e7f443a..e206984c794 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -837,8 +837,9 @@ void interpretert::execute_function_call()
   }
   else
   {
-    list_input_varst::iterator it=
-        function_input_vars.find(function_call.function().get(ID_identifier));
+    list_input_varst::iterator it = function_input_vars.find(
+      to_symbol_expr(function_call.function()).get_identifier());
+
     if(it!=function_input_vars.end())
     {
       mp_vectort value;
@@ -852,6 +853,7 @@ void interpretert::execute_function_call()
       it->second.pop_front();
       return;
     }
+
     if(show)
       error() << "no body for "+id2string(identifier) << eom;
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 517f66f050b..5344bcd6511 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -1083,10 +1083,9 @@ mp_integer interpretert::evaluate_address(
 {
   if(expr.id()==ID_symbol)
   {
-    const irep_idt &identifier=
-      is_ssa_expr(expr) ?
-      to_ssa_expr(expr).get_original_name() :
-      expr.get(ID_identifier);
+    const irep_idt &identifier = is_ssa_expr(expr)
+                                   ? to_ssa_expr(expr).get_original_name()
+                                   : to_symbol_expr(expr).get_identifier();
 
     interpretert::memory_mapt::const_iterator m_it1=
       memory_map.find(identifier);
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
index 5d69118a4a0..552de9cee29 100644
--- a/src/goto-programs/json_goto_trace.cpp
+++ b/src/goto-programs/json_goto_trace.cpp
@@ -107,7 +107,8 @@ void convert_decl(
       {
         if(expr.id() == ID_symbol)
         {
-          const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
+          const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
+
           if(expr.find(ID_C_base_name).is_not_nil())
             INVARIANT(
               expr.find(ID_C_base_name).id() == symbol.base_name,
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index 81e2812136b..d113af01230 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -72,8 +72,8 @@ exprt remove_const_function_pointerst::replace_const_symbols(
   {
     if(is_const_expression(expression))
     {
-      const symbolt &symbol=
-        *symbol_table.lookup(expression.get(ID_identifier));
+      const symbolt &symbol =
+        *symbol_table.lookup(to_symbol_expr(expression).get_identifier());
       if(symbol.type.id()!=ID_code)
       {
         const exprt &symbol_value=symbol.value;
diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp
index edb4c712ec2..fbb4d9d5947 100644
--- a/src/goto-programs/remove_unused_functions.cpp
+++ b/src/goto-programs/remove_unused_functions.cpp
@@ -81,9 +81,10 @@ void find_used_functions(
           // check that this is actually a simple call
           assert(call.function().id()==ID_symbol);
 
-          find_used_functions(call.function().get(ID_identifier),
-                              functions,
-                              seen);
+          const irep_idt &identifier =
+            to_symbol_expr(call.function()).get_identifier();
+
+          find_used_functions(identifier, functions, seen);
         }
       }
     }
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 23f7fea3f0b..dc19af71a89 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -375,8 +375,8 @@ void goto_symex_statet::propagationt::operator()(exprt &expr)
 {
   if(expr.id()==ID_symbol)
   {
-    valuest::const_iterator it=
-      values.find(expr.get(ID_identifier));
+    valuest::const_iterator it =
+      values.find(to_symbol_expr(expr).get_identifier());
     if(it!=values.end())
       expr=it->second;
   }
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index 2b1e096258c..57624a25d56 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -165,7 +165,7 @@ bool postconditiont::is_used(
   }
   else if(expr.id()==ID_symbol)
   {
-    return expr.get(ID_identifier)==identifier;
+    return to_symbol_expr(expr).get_identifier() == identifier;
   }
   else if(expr.id()==ID_dereference)
   {
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 9fe0036911d..747c56e3e00 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -538,8 +538,11 @@ std::set<exprt> symex_slice_by_tracet::implied_guards(exprt e)
 
   if(e.id()==ID_symbol)
   { // Guard or merge
-    const std::string &id_string=id2string(e.get(ID_identifier));
+    const std::string &id_string =
+      id2string(to_symbol_expr(e).get_identifier());
+
     std::string::size_type merge_loc=id_string.find("merge#");
+
     if(merge_loc==std::string::npos)
     {
       exprt e_copy(e);
diff --git a/src/memory-models/mm2cpp.cpp b/src/memory-models/mm2cpp.cpp
index 6492d8dae95..6ef3fe3bffc 100644
--- a/src/memory-models/mm2cpp.cpp
+++ b/src/memory-models/mm2cpp.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 class mm2cppt
 {
@@ -53,7 +54,7 @@ void mm2cppt::check_acyclic(const exprt &expr, unsigned indent)
 {
   if(expr.id()==ID_symbol)
   {
-    const irep_idt &identifier=expr.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(expr).get_identifier();
     let_valuest::const_iterator v_it=let_values.find(identifier);
     if(v_it!=let_values.end())
       check_acyclic(v_it->second, indent);
@@ -152,7 +153,7 @@ void mm2cppt::instruction2cpp(const codet &code, unsigned indent)
         assert(it->operands().size()==2);
         if(it->op0().id()==ID_symbol)
         {
-          irep_idt identifier=it->op0().get(ID_identifier);
+          irep_idt identifier = to_symbol_expr(it->op0()).get_identifier();
           let_values[identifier]=it->op1();
         }
         else
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 3b88a081984..96f371ef5cb 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -446,7 +446,7 @@ void value_set_fit::get_value_set_rec(
   {
     // just keep a reference to the ident in the set
     // (if it exists)
-    irep_idt ident = expr.get_string(ID_identifier)+suffix;
+    irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
     valuest::const_iterator v_it=values.find(ident);
 
     if(has_prefix(id2string(ident), alloc_adapter_prefix))
@@ -1229,7 +1229,7 @@ void value_set_fit::assign_rec(
   }
   else if(lhs.id()==ID_symbol)
   {
-    const irep_idt &identifier=lhs.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
 
     if(has_prefix(id2string(identifier),
                   "value_set::dynamic_object") ||
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 0c3a48fb088..3a54deac8f3 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -351,7 +351,7 @@ void value_set_fivrnst::get_value_set_rec(
   {
     // just keep a reference to the ident in the set
     // (if it exists)
-    irep_idt ident = expr.get_string(ID_identifier)+suffix;
+    irep_idt ident = id2string(to_symbol_expr(expr).get_identifier()) + suffix;
 
     if(has_prefix(id2string(ident), alloc_adapter_prefix))
     {
@@ -1012,7 +1012,7 @@ void value_set_fivrnst::assign_rec(
 
   if(lhs.id()==ID_symbol)
   {
-    const irep_idt &identifier=lhs.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(lhs).get_identifier();
 
     if(has_prefix(id2string(identifier),
                   "value_set::dynamic_object") ||
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index d32a2836aaf..f999c4beef7 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -53,16 +53,28 @@ class base_type_eqt
 void base_type_rec(
   typet &type, const namespacet &ns, std::set<irep_idt> &symb)
 {
-  if(type.id()==ID_symbol ||
-     type.id()==ID_c_enum_tag ||
-     type.id()==ID_struct_tag ||
-     type.id()==ID_union_tag)
+  if(type.id() == ID_symbol)
   {
     const symbolt *symbol;
 
-    if(!ns.lookup(type.get(ID_identifier), symbol) &&
-       symbol->is_type &&
-       !symbol->type.is_nil())
+    if(
+      !ns.lookup(to_symbol_type(type).get_identifier(), symbol) &&
+      symbol->is_type && !symbol->type.is_nil())
+    {
+      type = symbol->type;
+      base_type_rec(type, ns, symb); // recursive call
+      return;
+    }
+  }
+  else if(
+    type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
+    type.id() == ID_union_tag)
+  {
+    const symbolt *symbol;
+
+    if(
+      !ns.lookup(to_tag_type(type).get_identifier(), symbol) &&
+      symbol->is_type && !symbol->type.is_nil())
     {
       type=symbol->type;
       base_type_rec(type, ns, symb); // recursive call
@@ -87,12 +99,24 @@ void base_type_rec(
     typet &subtype=to_pointer_type(type).subtype();
 
     // we need to avoid running into an infinite loop
-    if(subtype.id()==ID_symbol ||
-       subtype.id()==ID_c_enum_tag ||
-       subtype.id()==ID_struct_tag ||
-       subtype.id()==ID_union_tag)
+    if(subtype.id() == ID_symbol)
+    {
+      const irep_idt &id = to_symbol_type(subtype).get_identifier();
+
+      if(symb.find(id) != symb.end())
+        return;
+
+      symb.insert(id);
+
+      base_type_rec(subtype, ns, symb);
+
+      symb.erase(id);
+    }
+    else if(
+      subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
+      subtype.id() == ID_union_tag)
     {
-      const irep_idt &id=subtype.get(ID_identifier);
+      const irep_idt &id = to_tag_type(subtype).get_identifier();
 
       if(symb.find(id)!=symb.end())
         return;
diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp
index 10adacba6c9..c78f856eb7c 100644
--- a/src/util/find_macros.cpp
+++ b/src/util/find_macros.cpp
@@ -10,8 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <stack>
 
-#include "expr.h"
 #include "namespace.h"
+#include "std_expr.h"
 #include "symbol.h"
 
 void find_macros(
@@ -29,8 +29,20 @@ void find_macros(
     const exprt &e=*stack.top();
     stack.pop();
 
-    if(e.id()==ID_symbol ||
-       e.id()==ID_next_symbol)
+    if(e.id() == ID_symbol)
+    {
+      const irep_idt &identifier = to_symbol_expr(e).get_identifier();
+
+      const symbolt &symbol = ns.lookup(identifier);
+
+      if(symbol.is_macro)
+      {
+        // inserted?
+        if(dest.insert(identifier).second)
+          stack.push(&symbol.value);
+      }
+    }
+    else if(e.id() == ID_next_symbol)
     {
       const irep_idt &identifier=e.get(ID_identifier);
 
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
index 9984ae584c2..2c6a596ba42 100644
--- a/src/util/find_symbols.cpp
+++ b/src/util/find_symbols.cpp
@@ -26,8 +26,9 @@ void find_symbols(
   bool current,
   bool next)
 {
-  if((src.id()==ID_symbol && current) ||
-     (src.id()==ID_next_symbol && next))
+  if(src.id() == ID_symbol && current)
+    dest.insert(to_symbol_expr(src).get_identifier());
+  else if(src.id() == ID_next_symbol && next)
     dest.insert(src.get(ID_identifier));
   else
   {
@@ -42,8 +43,9 @@ bool has_symbol(
   bool current,
   bool next)
 {
-  if((src.id()==ID_symbol && current) ||
-     (src.id()==ID_next_symbol && next))
+  if(src.id() == ID_symbol && current)
+    return symbols.count(to_symbol_expr(src).get_identifier()) != 0;
+  else if(src.id() == ID_next_symbol && next)
     return symbols.count(src.get(ID_identifier))!=0;
   else
   {
@@ -98,9 +100,12 @@ void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
   find_symbols(kind, src.type(), dest);
 
   if(kind==kindt::F_BOTH || kind==kindt::F_EXPR)
-    if(src.id()==ID_symbol ||
-       src.id()==ID_next_symbol)
+  {
+    if(src.id() == ID_symbol)
+      dest.insert(to_symbol_expr(src).get_identifier());
+    else if(src.id() == ID_next_symbol)
       dest.insert(src.get(ID_identifier));
+  }
 
   const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
 
@@ -161,7 +166,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
     }
   }
   else if(src.id()==ID_symbol)
-    dest.insert(src.get(ID_identifier));
+    dest.insert(to_symbol_type(src).get_identifier());
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
index bdd2ca799ba..32e9071bcce 100644
--- a/src/util/rename_symbol.cpp
+++ b/src/util/rename_symbol.cpp
@@ -94,7 +94,10 @@ bool rename_symbolt::have_to_rename(const exprt &dest) const
   // now do expression itself
 
   if(dest.id()==ID_symbol)
-    return expr_map.find(dest.get(ID_identifier))!=expr_map.end();
+  {
+    const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
+    return expr_map.find(identifier) != expr_map.end();
+  }
 
   forall_operands(it, dest)
     if(have_to_rename(*it))
@@ -251,7 +254,10 @@ bool rename_symbolt::have_to_rename(const typet &dest) const
     }
   }
   else if(dest.id()==ID_symbol)
-    return type_map.find(dest.get(ID_identifier))!=type_map.end();
+  {
+    const irep_idt &identifier = to_symbol_type(dest).get_identifier();
+    return type_map.find(identifier) != type_map.end();
+  }
   else if(dest.id()==ID_c_enum_tag ||
           dest.id()==ID_struct_tag ||
           dest.id()==ID_union_tag)
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index 25970620982..e568758661f 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -121,7 +121,10 @@ bool replace_symbolt::have_to_replace(const exprt &dest) const
   // now do expression itself
 
   if(dest.id()==ID_symbol)
-    return expr_map.find(dest.get(ID_identifier))!=expr_map.end();
+  {
+    const irep_idt &identifier = to_symbol_expr(dest).get_identifier();
+    return expr_map.find(identifier) != expr_map.end();
+  }
 
   forall_operands(it, dest)
     if(have_to_replace(*it))
@@ -184,8 +187,8 @@ bool replace_symbolt::replace(typet &dest) const
   }
   else if(dest.id()==ID_symbol)
   {
-    type_mapt::const_iterator it=
-      type_map.find(dest.get(ID_identifier));
+    type_mapt::const_iterator it =
+      type_map.find(to_symbol_type(dest).get_identifier());
 
     if(it!=type_map.end())
     {
@@ -248,7 +251,10 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
         return true;
   }
   else if(dest.id()==ID_symbol)
-    return type_map.find(dest.get(ID_identifier))!=type_map.end();
+  {
+    const irep_idt &identifier = to_symbol_type(dest).get_identifier();
+    return type_map.find(identifier) != type_map.end();
+  }
   else if(dest.id()==ID_array)
     return have_to_replace(to_array_type(dest).size());
 
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index fff9ba57f52..90e044c389d 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -439,9 +439,8 @@ bool simplify_exprt::simplify_inequality_address_of(exprt &expr)
   if(tmp0.op0().id()==ID_symbol &&
      tmp1.op0().id()==ID_symbol)
   {
-    bool equal=
-       tmp0.op0().get(ID_identifier)==
-       tmp1.op0().get(ID_identifier);
+    bool equal = to_symbol_expr(tmp0.op0()).get_identifier() ==
+                 to_symbol_expr(tmp1.op0()).get_identifier();
 
     expr.make_bool(expr.id()==ID_equal?equal:!equal);
 
@@ -627,7 +626,7 @@ tvt simplify_exprt::objects_equal_address_of(const exprt &a, const exprt &b)
 
   if(a.id()==ID_symbol && b.id()==ID_symbol)
   {
-    if(a.get(ID_identifier)==b.get(ID_identifier))
+    if(to_symbol_expr(a).get_identifier() == to_symbol_expr(b).get_identifier())
       return tvt(true);
   }
   else if(a.id()==ID_index && b.id()==ID_index)