diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
index b1467c205c0..c3972be4c2f 100644
--- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
+++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp
@@ -112,7 +112,7 @@ void ci_lazy_methods_neededt::gather_field_types(
   {
     // If class_type is not a symbol this may be a reference array,
     // but we can't tell what type.
-    if(class_type.id() == ID_symbol)
+    if(class_type.id() == ID_symbol_type)
     {
       const typet &element_type =
         java_array_element_type(to_symbol_type(class_type));
@@ -127,11 +127,11 @@ void ci_lazy_methods_neededt::gather_field_types(
   {
     for(const auto &field : underlying_type.components())
     {
-      if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
+      if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
         gather_field_types(field.type(), ns);
       else if(field.type().id() == ID_pointer)
       {
-        if(field.type().subtype().id() == ID_symbol)
+        if(field.type().subtype().id() == ID_symbol_type)
         {
           add_all_needed_classes(to_pointer_type(field.type()));
         }
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 21cac212cd4..1b223a80b14 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const typecast_exprt pointer(op[0], java_array_type(statement[0]));
 
       dereference_exprt array(pointer, pointer.type().subtype());
-      assert(pointer.type().subtype().id()==ID_symbol);
+      PRECONDITION(pointer.type().subtype().id() == ID_symbol_type);
       array.set(ID_java_member_access, true);
 
       const member_exprt length(array, "length", java_int_type());
@@ -2562,7 +2562,7 @@ codet java_bytecode_convert_methodt::convert_putstatic(
   const exprt::operandst &op,
   const symbol_exprt &symbol_expr)
 {
-  if(needed_lazy_methods && arg0.type().id() == ID_symbol)
+  if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
   {
     needed_lazy_methods->add_needed_class(
       to_symbol_type(arg0.type()).get_identifier());
@@ -2612,7 +2612,7 @@ void java_bytecode_convert_methodt::convert_getstatic(
 {
   if(needed_lazy_methods)
   {
-    if(arg0.type().id() == ID_symbol)
+    if(arg0.type().id() == ID_symbol_type)
     {
       needed_lazy_methods->add_needed_class(
         to_symbol_type(arg0.type()).get_identifier());
@@ -2620,7 +2620,7 @@ void java_bytecode_convert_methodt::convert_getstatic(
     else if(arg0.type().id() == ID_pointer)
     {
       const auto &pointer_type = to_pointer_type(arg0.type());
-      if(pointer_type.subtype().id() == ID_symbol)
+      if(pointer_type.subtype().id() == ID_symbol_type)
       {
         needed_lazy_methods->add_needed_class(
           to_symbol_type(pointer_type.subtype()).get_identifier());
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
index 75698dc0d31..903024e91ae 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp
@@ -117,7 +117,7 @@ java_bytecode_parse_treet::find_annotation(
       if(annotation.type.id() != ID_pointer)
         return false;
       const typet &type = annotation.type.subtype();
-      return type.id() == ID_symbol &&
+      return type.id() == ID_symbol_type &&
              to_symbol_type(type).get_identifier() == annotation_type_name;
     });
   if(annotation_it == annotations.end())
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index ef41a7366f4..40b46bcd346 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -616,7 +616,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
     for(const auto &p : ct.parameters())
       get_class_refs_rec(p.type());
   }
-  else if(src.id()==ID_symbol)
+  else if(src.id()==ID_symbol_type)
   {
     irep_idt name=src.get(ID_C_base_name);
     if(has_prefix(id2string(name), "array["))
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
index 2f26feb59bc..ecfb83a47ca 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp
@@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void java_bytecode_typecheckt::typecheck_type(typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     irep_idt identifier=to_symbol_type(type).get_identifier();
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index d9461898a10..7007def5165 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1179,7 +1179,7 @@ void java_object_factoryt::gen_nondet_init(
     if(is_sub)
     {
       const typet &symbol = override_ ? override_type : expr.type();
-      PRECONDITION(symbol.id() == ID_symbol);
+      PRECONDITION(symbol.id() == ID_symbol_type);
       generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
         to_symbol_type(symbol), struct_type);
     }
@@ -1286,7 +1286,7 @@ void java_object_factoryt::gen_nondet_array_init(
   const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
-  PRECONDITION(expr.type().subtype().id()==ID_symbol);
+  PRECONDITION(expr.type().subtype().id() == ID_symbol_type);
   PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
 
   const typet &type=ns.follow(expr.type().subtype());
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index e7c8c8058c7..d6fa7bfdaca 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -36,7 +36,7 @@ Date:   April 2017
 irep_idt get_tag(const typet &type)
 {
   /// \todo Use follow instead of assuming tag to symbol relationship.
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
     return to_symbol_type(type).get_identifier();
   else if(type.id() == ID_struct)
     return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
@@ -394,11 +394,11 @@ java_string_library_preprocesst::process_equals_function_operands(
 /// \return type of the "data" component
 static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
 {
-  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
-  if(type.id()==ID_symbol)
+  PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
+  if(type.id() == ID_symbol_type)
   {
     symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
-    CHECK_RETURN(sym.type.id()!=ID_symbol);
+    CHECK_RETURN(sym.type.id() != ID_symbol_type);
     return get_data_type(sym.type, symbol_table);
   }
   // else type id is ID_struct
@@ -413,11 +413,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
 static typet
 get_length_type(const typet &type, const symbol_tablet &symbol_table)
 {
-  PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
-  if(type.id()==ID_symbol)
+  PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
+  if(type.id() == ID_symbol_type)
   {
     symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
-    CHECK_RETURN(sym.type.id()!=ID_symbol);
+    CHECK_RETURN(sym.type.id() != ID_symbol_type);
     return get_length_type(sym.type, symbol_table);
   }
   // else type id is ID_struct
@@ -892,7 +892,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
   PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
 
   typet deref_type;
-  if(rhs.type().subtype().id()==ID_symbol)
+  if(rhs.type().subtype().id() == ID_symbol_type)
     deref_type=symbol_table.lookup_ref(
       to_symbol_type(rhs.type().subtype()).get_identifier()).type;
   else
diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index 67e3a27e971..2d775c05293 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -777,7 +777,8 @@ bool equal_java_types(const typet &type1, const typet &type2)
   bool arrays_with_same_element_type = true;
   if(
     type1.id() == ID_pointer && type2.id() == ID_pointer &&
-    type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
+    type1.subtype().id() == ID_symbol_type &&
+    type2.subtype().id() == ID_symbol_type)
   {
     const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
     const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
@@ -824,7 +825,7 @@ void get_dependencies_from_generic_parameters_rec(
   }
 
   // symbol type
-  else if(t.id() == ID_symbol)
+  else if(t.id() == ID_symbol_type)
   {
     const symbol_typet &symbol_type = to_symbol_type(t);
     const irep_idt class_name(symbol_type.get_identifier());
@@ -958,7 +959,7 @@ std::string pretty_java_type(const typet &type)
     return "byte";
   else if(is_reference(type))
   {
-    if(type.subtype().id() == ID_symbol)
+    if(type.subtype().id() == ID_symbol_type)
     {
       const auto &symbol_type = to_symbol_type(type.subtype());
       const irep_idt &id = symbol_type.get_identifier();
diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp
index d980983bf41..dbacbac4a04 100644
--- a/jbmc/src/java_bytecode/remove_instanceof.cpp
+++ b/jbmc/src/java_bytecode/remove_instanceof.cpp
@@ -85,7 +85,7 @@ bool remove_instanceoft::lower_instanceof(
 
   // Find all types we know about that satisfy the given requirement:
   INVARIANT(
-    target_type.id()==ID_symbol,
+    target_type.id() == ID_symbol_type,
     "instanceof second operand should have a simple type");
   const irep_idt &target_name=
     to_symbol_type(target_type).get_identifier();
diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp
index 6059b1e5084..e9b69ba002a 100644
--- a/jbmc/src/java_bytecode/select_pointer_type.cpp
+++ b/jbmc/src/java_bytecode/select_pointer_type.cpp
@@ -108,7 +108,7 @@ pointer_typet select_pointer_typet::specialize_generics(
     visited_nodes.erase(parameter_name);
     return returned_type;
   }
-  else if(pointer_type.subtype().id() == ID_symbol)
+  else if(pointer_type.subtype().id() == ID_symbol_type)
   {
     // if the pointer is an array, recursively specialize its element type
     const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());
diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp
index 77d09d02bc8..a3079048a33 100644
--- a/jbmc/unit/java-testing-utils/require_type.cpp
+++ b/jbmc/unit/java-testing-utils/require_type.cpp
@@ -427,7 +427,7 @@ require_type::require_complete_java_non_generic_class(const typet &class_type)
 const symbol_typet &
 require_type::require_symbol(const typet &type, const irep_idt &identifier)
 {
-  REQUIRE(type.id() == ID_symbol);
+  REQUIRE(type.id() == ID_symbol_type);
   const symbol_typet &result = to_symbol_type(type);
   if(identifier != "")
   {
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 98dc10b63ed..296e2ffaf11 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
@@ -63,7 +63,7 @@ SCENARIO(
         next.type(),
         {{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
          {require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
-    REQUIRE(next_type.subtype().id() == ID_symbol);
+    REQUIRE(next_type.subtype().id() == ID_symbol_type);
     const symbol_typet &next_symbol = to_symbol_type(next_type.subtype());
     REQUIRE(
       symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
@@ -75,7 +75,7 @@ SCENARIO(
         reverse.type(),
         {{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
          {require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
-    REQUIRE(next_type.subtype().id() == ID_symbol);
+    REQUIRE(next_type.subtype().id() == ID_symbol_type);
     const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype());
     REQUIRE(
       symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel
index 11593f7dcf1..0ddb17184a5 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_bad/object.intel and b/regression/ansi-c/arch_flags_mcpu_bad/object.intel differ
diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm
index 9ac75ab47a9..d417b14bad4 100644
Binary files a/regression/ansi-c/arch_flags_mcpu_good/object.arm and b/regression/ansi-c/arch_flags_mcpu_good/object.arm differ
diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm
index 86bbebb1240..d0104c3b605 100644
Binary files a/regression/ansi-c/arch_flags_mthumb_good/object.arm and b/regression/ansi-c/arch_flags_mthumb_good/object.arm differ
diff --git a/regression/goto-diff/syntactic-diff1/a.gb b/regression/goto-diff/syntactic-diff1/a.gb
index 2bf7c7b9947..0cfbfe7718c 100644
Binary files a/regression/goto-diff/syntactic-diff1/a.gb and b/regression/goto-diff/syntactic-diff1/a.gb differ
diff --git a/regression/goto-diff/syntactic-diff1/b.gb b/regression/goto-diff/syntactic-diff1/b.gb
index b1db4ddb9e3..98582db0d43 100644
Binary files a/regression/goto-diff/syntactic-diff1/b.gb and b/regression/goto-diff/syntactic-diff1/b.gb differ
diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
index e89a21529e7..8bcd917a6bf 100644
--- a/src/analyses/invariant_propagation.cpp
+++ b/src/analyses/invariant_propagation.cpp
@@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const
     return false;
   else if(type.id()==ID_array)
     return false;
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return check_type(ns.follow(type));
   else if(type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index 21e4c47ec67..e41f93dae4e 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
 {
   PRECONDITION(type.id()==ID_pointer);
 
-  if(type.subtype().id()==ID_symbol)
-  {
+  if(type.subtype().id() == ID_symbol_type)
     return to_symbol_type(type.subtype()).get_identifier();
-  }
-  return ID_empty;
+  else
+    return ID_empty;
 }
 
 /// Returns the symbol corresponding to an exception
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index b0f3aeda819..746a01cb834 100644
--- a/src/ansi-c/c_typecast.cpp
+++ b/src/ansi-c/c_typecast.cpp
@@ -253,7 +253,8 @@ bool check_c_implicit_typecast(
 typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 {
   if(
-    src_type.id() != ID_symbol && src_type.id() != ID_struct_tag &&
+    src_type.id() != ID_symbol_type &&
+    src_type.id() != ID_struct_tag &&
     src_type.id() != ID_union_tag)
   {
     return src_type;
@@ -264,7 +265,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
   // collect qualifiers
   c_qualifierst qualifiers(src_type);
 
-  while(result_type.id() == ID_symbol || result_type.id() == ID_struct_tag ||
+  while(result_type.id() == ID_symbol_type ||
+        result_type.id() == ID_struct_tag ||
         result_type.id() == ID_union_tag)
   {
     const typet &followed_type = ns.follow(result_type);
@@ -348,7 +350,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   {
     return INT;
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return get_c_type(ns.follow(type));
   else if(type.id()==ID_rational)
     return RATIONAL;
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index ee120fe00fd..8b158712237 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -406,7 +406,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
        final_old.subtype()==final_new.subtype())
     {
       // we don't do symbol types for arrays anymore
-      PRECONDITION(old_symbol.type.id()!=ID_symbol);
+      PRECONDITION(old_symbol.type.id() != ID_symbol_type);
       old_symbol.type=new_symbol.type;
     }
     else if((final_old.id()==ID_incomplete_c_enum ||
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index be2d711416d..0ce2899c793 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -383,7 +383,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
   }
   else if(type.id()==ID_vector)
     return is_complete_type(type.subtype());
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     return is_complete_type(follow(type));
 
   return true;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index b8b0e7fe595..d30aa74e270 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -91,9 +91,9 @@ bool c_typecheck_baset::gcc_types_compatible_p(
   // read
   // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
 
-  if(type1.id()==ID_symbol)
+  if(type1.id() == ID_symbol_type)
     return gcc_types_compatible_p(follow(type1), type2);
-  else if(type2.id()==ID_symbol)
+  else if(type2.id() == ID_symbol_type)
     return gcc_types_compatible_p(type1, follow(type2));
 
   // check qualifiers first
@@ -3067,8 +3067,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
 
   typet subtype=type.subtype();
 
-  if(subtype.id()==ID_symbol)
-    subtype=follow(subtype);
+  if(subtype.id() == ID_symbol_type)
+    subtype = follow(to_symbol_type(subtype));
 
   if(subtype.id()==ID_incomplete_struct)
   {
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index 977ad82f43f..ad1be10fe07 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
     const typet &type=designator.back().subtype;
     const typet &full_type=follow(type);
-    assert(full_type.id()!=ID_symbol);
+    CHECK_RETURN(full_type.id() != ID_symbol_type);
 
     // do we initialize a scalar?
     if(full_type.id()!=ID_struct &&
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index c6767fb40e1..ad092c42e42 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -89,7 +89,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
     typecheck_c_bit_field_type(to_c_bit_field_type(type));
   else if(type.id()==ID_typeof)
     typecheck_typeof_type(type);
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
     typecheck_symbol_type(to_symbol_type(type));
   else if(type.id() == ID_typedef_type)
     typecheck_typedef_type(type);
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 80b5515dd0f..c1327cdd807 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -457,7 +457,7 @@ std::string expr2ct::convert_rec(
     return convert_rec(
       src.subtype(), qualifiers, declarator+"[]");
   }
-  else if(src.id()==ID_symbol)
+  else if(src.id() == ID_symbol_type)
   {
     symbol_typet symbolic_type=to_symbol_type(src);
     const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index 78489fde8ab..ba4771f97ba 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -86,8 +86,8 @@ mp_integer alignment(const typet &type, const namespacet &ns)
     result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
   else if(type.id() == ID_union_tag)
     result = alignment(ns.follow_tag(to_union_tag_type(type)), ns);
-  else if(type.id()==ID_symbol)
-    result=alignment(ns.follow(type), ns);
+  else if(type.id() == ID_symbol_type)
+    result = alignment(ns.follow(to_symbol_type(type)), ns);
   else if(type.id()==ID_c_bit_field)
   {
     // we align these according to the 'underlying type'
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index b17d92752fe..87789b6c457 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -187,10 +187,9 @@ static std::string type2name(
     else
       result+="ARR"+integer2string(size);
   }
-  else if(type.id()==ID_symbol ||
-          type.id()==ID_c_enum_tag ||
-          type.id()==ID_struct_tag ||
-          type.id()==ID_union_tag)
+  else if(
+    type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||
+    type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
     parent_is_sym_check=true;
     result+=type2name_symbol(type, ns, symbol_number);
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
index e3dcadddea7..3f0b445fc59 100644
--- a/src/cpp/cpp_convert_type.cpp
+++ b/src/cpp/cpp_convert_type.cpp
@@ -588,19 +588,13 @@ void cpp_convert_typet::write(typet &type)
 
 void cpp_convert_plain_type(typet &type)
 {
-  if(type.id()==ID_cpp_name ||
-     type.id()==ID_struct ||
-     type.id()==ID_union ||
-     type.id()==ID_array ||
-     type.id()==ID_code ||
-     type.id()==ID_unsignedbv ||
-     type.id()==ID_signedbv ||
-     type.id()==ID_bool ||
-     type.id()==ID_floatbv ||
-     type.id()==ID_empty ||
-     type.id()==ID_symbol ||
-     type.id()==ID_constructor ||
-     type.id()==ID_destructor)
+  if(
+    type.id() == ID_cpp_name || type.id() == ID_struct ||
+    type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
+    type.id() == ID_symbol_type || type.id() == ID_constructor ||
+    type.id() == ID_destructor)
   {
   }
   else if(type.id()==ID_c_enum)
diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp
index 880d05fe2ef..800faa07aa6 100644
--- a/src/cpp/cpp_declarator_converter.cpp
+++ b/src/cpp/cpp_declarator_converter.cpp
@@ -141,8 +141,9 @@ symbolt &cpp_declarator_convertert::convert(
           cpp_typecheck_resolvet::wantt::TYPE,
           cpp_typecheck_fargst());
 
-      if(symbol_expr.id()!=ID_type ||
-         symbol_expr.type().id()!=ID_symbol)
+      if(
+        symbol_expr.id() != ID_type ||
+        symbol_expr.type().id() != ID_symbol_type)
       {
         cpp_typecheck.error().source_location=name.source_location();
         cpp_typecheck.error() << "error: expected type"
diff --git a/src/cpp/cpp_exception_id.cpp b/src/cpp/cpp_exception_id.cpp
index aef6606a4bd..f06f221f3c5 100644
--- a/src/cpp/cpp_exception_id.cpp
+++ b/src/cpp/cpp_exception_id.cpp
@@ -20,7 +20,7 @@ void cpp_exception_list_rec(
   const std::string &suffix,
   std::vector<irep_idt> &dest)
 {
-  if(src.id()==ID_symbol)
+  if(src.id() == ID_symbol_type)
   {
     cpp_exception_list_rec(ns.follow(src), ns, suffix, dest);
   }
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
index b47a864814e..93c6ee2e602 100644
--- a/src/cpp/cpp_instantiate_template.cpp
+++ b/src/cpp/cpp_instantiate_template.cpp
@@ -50,8 +50,8 @@ std::string cpp_typecheckt::template_suffix(
     if(expr.id()==ID_type)
     {
       const typet &type=expr.type();
-      if(type.id()==ID_symbol)
-        result+=type.get_string(ID_identifier);
+      if(type.id() == ID_symbol_type)
+        result += id2string(to_symbol_type(type).get_identifier());
       else
         result+=cpp_type2name(type);
     }
@@ -190,7 +190,7 @@ const symbolt &cpp_typecheckt::class_template_symbol(
 void cpp_typecheckt::elaborate_class_template(
   const typet &type)
 {
-  if(type.id()!=ID_symbol)
+  if(type.id() != ID_symbol_type)
     return;
 
   const symbolt &symbol = lookup(to_symbol_type(type));
diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp
index 5ea145f505f..1f4ceee38a8 100644
--- a/src/cpp/cpp_is_pod.cpp
+++ b/src/cpp/cpp_is_pod.cpp
@@ -80,7 +80,7 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const
     // but pointers are PODs!
     return true;
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     const symbolt &symb = lookup(to_symbol_type(type));
     DATA_INVARIANT(symb.is_type, "type symbol is a type");
diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp
index a9cabf3c112..6870a5cf3b1 100644
--- a/src/cpp/cpp_typecheck_bases.cpp
+++ b/src/cpp/cpp_typecheck_bases.cpp
@@ -44,7 +44,7 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type)
     // elaborate any class template instances given as bases
     elaborate_class_template(base_symbol_expr.type());
 
-    if(base_symbol_expr.type().id()!=ID_symbol)
+    if(base_symbol_expr.type().id() != ID_symbol_type)
     {
       error().source_location=name.source_location();
       error() << "expected type symbol as struct/class base" << eom;
diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp
index f89ca87cc55..0422bcfffab 100644
--- a/src/cpp/cpp_typecheck_compound_type.cpp
+++ b/src/cpp/cpp_typecheck_compound_type.cpp
@@ -889,7 +889,7 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
     // TODO
     //    typecheck_type(ftype);
-    //    assert(ftype.id()==ID_symbol);
+    //    assert(ftype.id()==ID_symbol_type);
     //    symbol.type.add("ID_C_friends").move_to_sub(ftype);
 
     return;
@@ -1631,7 +1631,7 @@ void cpp_typecheckt::get_bases(
   forall_irep(it, bases)
   {
     assert(it->id()==ID_base);
-    assert(it->get(ID_type)==ID_symbol);
+    assert(it->get(ID_type) == ID_symbol_type);
 
     const struct_typet &base=
       to_struct_type(lookup(it->find(ID_type).get(ID_identifier)).type);
@@ -1653,7 +1653,7 @@ void cpp_typecheckt::get_virtual_bases(
   forall_irep(it, bases)
   {
     assert(it->id()==ID_base);
-    assert(it->get(ID_type)==ID_symbol);
+    assert(it->get(ID_type) == ID_symbol_type);
 
     const struct_typet &base=
       to_struct_type(lookup(it->find(ID_type).get(ID_identifier)).type);
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index b89b7460a39..d9d9ec2e3e3 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -252,7 +252,7 @@ void cpp_typecheckt::default_cpctor(
   forall_irep(parent_it, bases.get_sub())
   {
     assert(parent_it->id()==ID_base);
-    assert(parent_it->get(ID_type)==ID_symbol);
+    assert(parent_it->get(ID_type) == ID_symbol_type);
 
     const symbolt &parsymb=
       lookup(parent_it->find(ID_type).get(ID_identifier));
@@ -367,7 +367,7 @@ void cpp_typecheckt::default_assignop(
   std::string arg_name("ref");
 
   cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec);
-  cpctor.type().id(ID_symbol);
+  cpctor.type().id(ID_symbol_type);
   cpctor.type().add(ID_identifier).id(symbol.name);
   cpctor.operands().push_back(exprt(ID_cpp_declarator));
   cpctor.add_source_location()=source_location;
@@ -447,7 +447,7 @@ void cpp_typecheckt::default_assignop_value(
   forall_irep(parent_it, bases.get_sub())
   {
     assert(parent_it->id()==ID_base);
-    assert(parent_it->get(ID_type)==ID_symbol);
+    assert(parent_it->get(ID_type) == ID_symbol_type);
 
     const symbolt &symb=
       lookup(parent_it->find(ID_type).get(ID_identifier));
@@ -540,7 +540,7 @@ void cpp_typecheckt::check_member_initializers(
       bool ok=false;
       forall_irep(parent_it, bases.get_sub())
       {
-        assert(parent_it->get(ID_type)==ID_symbol);
+        assert(parent_it->get(ID_type) == ID_symbol_type);
 
         if(member_type.get(ID_identifier)
           ==parent_it->find(ID_type).get(ID_identifier))
@@ -584,7 +584,7 @@ void cpp_typecheckt::check_member_initializers(
       if(c_it->get_bool("is_type"))
       {
         typet type=static_cast<const typet&>(c_it->find(ID_type));
-        if(type.id()!=ID_symbol)
+        if(type.id() != ID_symbol_type)
           continue;
 
         const symbolt &symb=lookup(type.get(ID_identifier));
@@ -594,7 +594,7 @@ void cpp_typecheckt::check_member_initializers(
         // check for a direct parent
         forall_irep(parent_it, bases.get_sub())
         {
-          assert(parent_it->get(ID_type)==ID_symbol);
+          assert(parent_it->get(ID_type) == ID_symbol_type);
           if(symb.name==parent_it->find(ID_type).get(ID_identifier))
           {
             ok=true;
@@ -617,7 +617,7 @@ void cpp_typecheckt::check_member_initializers(
         // check for a direct parent
         forall_irep(parent_it, bases.get_sub())
         {
-          assert(parent_it->get(ID_type)==ID_symbol);
+          assert(parent_it->get(ID_type) == ID_symbol_type);
 
           if(member_type.get(ID_identifier)==
              parent_it->find(ID_type).get(ID_identifier))
@@ -711,7 +711,7 @@ void cpp_typecheckt::full_member_initialization(
     forall_irep(parent_it, bases.get_sub())
     {
       assert(parent_it->id()==ID_base);
-      assert(parent_it->get(ID_type)==ID_symbol);
+      assert(parent_it->get(ID_type) == ID_symbol_type);
 
       const symbolt &ctorsymb=
         lookup(parent_it->find(ID_type).get(ID_identifier));
@@ -764,7 +764,7 @@ void cpp_typecheckt::full_member_initialization(
 
         typecheck_type(member_type);
 
-        if(member_type.id()!=ID_symbol)
+        if(member_type.id() != ID_symbol_type)
           break;
 
         if(parent_it->find(ID_type).get(ID_identifier)==
diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp
index 193dede0a8f..8f66277be04 100644
--- a/src/cpp/cpp_typecheck_destructor.cpp
+++ b/src/cpp/cpp_typecheck_destructor.cpp
@@ -160,7 +160,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol)
       bit++)
   {
     assert(bit->id()==ID_base);
-    assert(bit->find(ID_type).id()==ID_symbol);
+    assert(bit->find(ID_type).id() == ID_symbol_type);
     const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier));
 
     symbol_exprt this_ptr(ID_this, pointer_type(symbol.type));
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 2ffd3524407..9cb17f46b33 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -605,8 +605,9 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr)
 
       // TODO: need to resolve an incomplete struct (template) here
       // go into scope of first operand
-      if(expr.op0().type().id()==ID_symbol &&
-         follow(expr.op0().type()).id()==ID_struct)
+      if(
+        expr.op0().type().id() == ID_symbol_type &&
+        follow(expr.op0().type()).id() == ID_struct)
       {
         const irep_idt &struct_identifier=
           expr.op0().type().get(ID_identifier);
diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp
index 484fc458712..42c0ac58ed4 100644
--- a/src/cpp/cpp_typecheck_resolve.cpp
+++ b/src/cpp/cpp_typecheck_resolve.cpp
@@ -174,7 +174,7 @@ void cpp_typecheck_resolvet::remove_duplicates(
 
     if(it->id()==ID_symbol)
       id = to_symbol_expr(*it).get_identifier();
-    else if(it->id()==ID_type && it->type().id()==ID_symbol)
+    else if(it->id() == ID_type && it->type().id() == ID_symbol_type)
       id = to_symbol_type(it->type()).get_identifier();
 
     if(id=="")
@@ -362,7 +362,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
       typet followed_type=symbol.type;
       bool constant=followed_type.get_bool(ID_C_constant);
 
-      while(followed_type.id()==ID_symbol)
+      while(followed_type.id() == ID_symbol_type)
       {
         followed_type =
           cpp_typecheck.follow(to_symbol_type(followed_type));
@@ -2285,7 +2285,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
         assert(pcomp.get_bool(ID_is_type));
         const typet &type=pcomp.type();
         assert(type.id()!=ID_struct);
-        if(type.id()==ID_symbol)
+
+        if(type.id() == ID_symbol_type)
           identifier = to_symbol_type(type).get_identifier();
         else
           continue;
@@ -2307,7 +2308,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           new_set.insert(&class_id);
           break;
         }
-        else if(symbol.type.id()==ID_symbol)
+        else if(symbol.type.id() == ID_symbol_type)
           identifier = to_symbol_type(symbol.type).get_identifier();
         else
           break;
@@ -2350,7 +2351,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
       if(e.id()!=ID_type)
         continue; // expressions are definitively not a scope
 
-      if(e.type().id()==ID_symbol)
+      if(e.type().id() == ID_symbol_type)
       {
         symbol_typet type=to_symbol_type(e.type());
 
@@ -2361,7 +2362,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           const symbolt &symbol=cpp_typecheck.lookup(identifier);
           assert(symbol.is_type);
 
-          if(symbol.type.id()==ID_symbol)
+          if(symbol.type.id() == ID_symbol_type)
             type=to_symbol_type(symbol.type);
           else if(symbol.type.id()==ID_struct ||
                   symbol.type.id()==ID_incomplete_struct ||
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
index 052be288891..0281e0fea24 100644
--- a/src/cpp/cpp_typecheck_template.cpp
+++ b/src/cpp/cpp_typecheck_template.cpp
@@ -786,8 +786,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
     // is it a type or not?
     if(declaration.get_bool(ID_is_type))
     {
-      parameter=exprt(ID_type, typet(ID_symbol));
-      parameter.type().set(ID_identifier, identifier);
+      parameter = exprt(ID_type, symbol_typet(identifier));
       parameter.type().add_source_location()=declaration.find_source_location();
     }
     else
@@ -822,8 +821,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
 
     if(cpp_declarator_converter.is_typedef)
     {
-      parameter=exprt(ID_type, typet(ID_symbol));
-      parameter.type().set(ID_identifier, symbol.name);
+      parameter = exprt(ID_type, symbol_typet(symbol.name));
       parameter.type().add_source_location()=declaration.find_location();
     }
     else
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index cb8dfe198ba..8bab226bde4 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -186,7 +186,7 @@ void cpp_typecheckt::typecheck_type(typet &type)
           type.id()==ID_empty)
   {
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
   }
   else if(type.id()==ID_constructor ||
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
index 7d483bd1b05..24db086866a 100644
--- a/src/cpp/expr2cpp.cpp
+++ b/src/cpp/expr2cpp.cpp
@@ -187,7 +187,7 @@ std::string expr2cppt::convert_rec(
     else
       return expr2ct::convert_rec(src, qualifiers, declarator);
   }
-  else if(src.id()==ID_symbol)
+  else if(src.id() == ID_symbol_type)
   {
     const irep_idt &identifier=
       to_symbol_type(src).get_identifier();
diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp
index 02d901e391f..28bbb632834 100644
--- a/src/cpp/template_map.cpp
+++ b/src/cpp/template_map.cpp
@@ -39,7 +39,7 @@ void template_mapt::apply(typet &type) const
       apply(subtype);
     }
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     type_mapt::const_iterator m_it =
       type_map.find(to_symbol_type(type).get_identifier());
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 2715f303063..baecc693418 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -61,8 +61,7 @@ void dump_ct::operator()(std::ostream &os)
     {
       typet &type=it2->type();
 
-      if(type.id()==ID_symbol &&
-         type.get_bool(ID_C_transparent_union))
+      if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
       {
         symbolt new_type_sym=
           ns.lookup(to_symbol_type(type).get_identifier());
@@ -314,7 +313,7 @@ void dump_ct::convert_compound(
   bool recursive,
   std::ostream &os)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
@@ -382,7 +381,7 @@ void dump_ct::convert_compound(
     UNREACHABLE;
     /*
     assert(parent_it->id() == ID_base);
-    assert(parent_it->get(ID_type) == ID_symbol);
+    assert(parent_it->get(ID_type) == ID_symbol_type);
 
     const irep_idt &base_id=
       parent_it->find(ID_type).get(ID_identifier);
@@ -669,7 +668,7 @@ void dump_ct::collect_typedefs_rec(
   {
     collect_typedefs_rec(type.subtype(), early, local_deps);
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 5f8a4b00c74..a634b081a19 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1422,7 +1422,7 @@ goto_programt::const_targett goto_program2codet::convert_catch(
 
 void goto_program2codet::add_local_types(const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     const typet &full_type=ns.follow(type);
 
@@ -1655,7 +1655,7 @@ void goto_program2codet::remove_const(typet &type)
   if(type.get_bool(ID_C_constant))
     type.remove(ID_C_constant);
 
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     const irep_idt &identifier=to_symbol_type(type).get_identifier();
     if(!const_removed.insert(identifier).second)
@@ -1861,7 +1861,8 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     if(no_typecast)
       return;
 
-    assert(expr.type().id()==ID_symbol);
+    DATA_INVARIANT(expr.type().id() == ID_symbol_type,
+                   "type of union/struct expressions");
 
     const typet &t=expr.type();
 
diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp
index cc6b14c0d2b..db13c0ea3a5 100644
--- a/src/goto-programs/destructor.cpp
+++ b/src/goto-programs/destructor.cpp
@@ -19,7 +19,7 @@ code_function_callt get_destructor(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     return get_destructor(ns, ns.follow(type));
   }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 4ec0c2ac729..7136eec4509 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -1043,10 +1043,11 @@ mp_integer interpretert::get_size(const typet &type)
     }
     return subtype_size;
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     return get_size(ns.follow(type));
   }
+
   return 1;
 }
 
diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp
index b3f868e50ff..0543c0d2ad9 100644
--- a/src/goto-programs/read_bin_goto_object.cpp
+++ b/src/goto-programs/read_bin_goto_object.cpp
@@ -20,10 +20,10 @@ Date: June 2006
 
 #include "goto_functions.h"
 
-/// read goto binary format v3
+/// read goto binary format v4
 /// \par parameters: input stream, symbol_table, functions
 /// \return true on error, false otherwise
-static bool read_bin_goto_object_v3(
+static bool read_bin_goto_object_v4(
   std::istream &in,
   symbol_tablet &symbol_table,
   goto_functionst &functions,
@@ -221,13 +221,14 @@ bool read_bin_goto_object(
     {
     case 1:
     case 2:
+    case 3:
       message.error() <<
           "The input was compiled with an old version of "
           "goto-cc; please recompile" << messaget::eom;
       return true;
 
-    case 3:
-      return read_bin_goto_object_v3(
+    case 4:
+      return read_bin_goto_object_v4(
         in, symbol_table, functions, irepconverter);
       break;
 
diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h
index c79ec5154fe..da78ecd3779 100644
--- a/src/goto-programs/string_abstraction.h
+++ b/src/goto-programs/string_abstraction.h
@@ -52,7 +52,7 @@ class string_abstractiont:public messaget
 
   bool is_char_type(const typet &type) const
   {
-    if(type.id()==ID_symbol)
+    if(type.id() == ID_symbol_type)
       return is_char_type(ns.follow(type));
 
     if(type.id()!=ID_signedbv &&
diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp
index a6d0f144cb2..3ab58528319 100644
--- a/src/goto-programs/write_goto_binary.cpp
+++ b/src/goto-programs/write_goto_binary.cpp
@@ -19,8 +19,8 @@ Author: CM Wintersteiger
 
 #include <goto-programs/goto_model.h>
 
-/// Writes a goto program to disc, using goto binary format ver 2
-bool write_goto_binary_v3(
+/// Writes a goto program to disc, using goto binary format ver 4
+bool write_goto_binary_v4(
   std::ostream &out,
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
@@ -151,13 +151,12 @@ bool write_goto_binary(
   switch(version)
   {
   case 1:
-    throw "version 1 no longer supported";
-
   case 2:
-    throw "version 2 no longer supported";
-
   case 3:
-    return write_goto_binary_v3(
+    throw "version no longer supported";
+
+  case 4:
+    return write_goto_binary_v4(
       out, symbol_table, goto_functions, irepconverter);
 
   default:
diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h
index d9cf23d6def..c700f41cc04 100644
--- a/src/goto-programs/write_goto_binary.h
+++ b/src/goto-programs/write_goto_binary.h
@@ -12,7 +12,7 @@ Author: CM Wintersteiger
 #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
 
-#define GOTO_BINARY_VERSION 3
+#define GOTO_BINARY_VERSION 4
 
 #include <iosfwd>
 #include <string>
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index e306a86d13d..1cc7de3e427 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -760,7 +760,7 @@ void goto_symex_statet::rename_address(
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
-      if(member_expr.struct_op().type().id()!=ID_symbol)
+      if(member_expr.struct_op().type().id() != ID_symbol_type)
       {
         const struct_union_typet &su_type=
           to_struct_union_type(member_expr.struct_op().type());
@@ -843,7 +843,7 @@ void goto_symex_statet::rename(
   {
     rename(type.subtype(), irep_idt(), ns, level);
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 4e480e7570f..f39b1a9666e 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -44,7 +44,7 @@ static const typet &follow_tags_symbols(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return ns.follow(type);
   else if(type.id()==ID_c_enum_tag)
     return ns.follow_tag(to_c_enum_tag_type(type));
@@ -790,10 +790,9 @@ bool linkingt::adjust_object_type_rec(
   if(base_type_eq(t1, t2, ns))
     return false;
 
-  if(t1.id()==ID_symbol ||
-     t1.id()==ID_struct_tag ||
-     t1.id()==ID_union_tag ||
-     t1.id()==ID_c_enum_tag)
+  if(
+    t1.id() == ID_symbol_type || t1.id() == ID_struct_tag ||
+    t1.id() == ID_union_tag || t1.id() == ID_c_enum_tag)
   {
     const irep_idt &identifier=t1.get(ID_identifier);
 
@@ -808,10 +807,9 @@ bool linkingt::adjust_object_type_rec(
 
     return false;
   }
-  else if(t2.id()==ID_symbol ||
-          t2.id()==ID_struct_tag ||
-          t2.id()==ID_union_tag ||
-          t2.id()==ID_c_enum_tag)
+  else if(
+    t2.id() == ID_symbol_type || t2.id() == ID_struct_tag ||
+    t2.id() == ID_union_tag || t2.id() == ID_c_enum_tag)
   {
     const irep_idt &identifier=t2.get(ID_identifier);
 
diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp
index 85ac59305f5..30ae4748ab9 100644
--- a/src/solvers/refinement/string_refinement_util.cpp
+++ b/src/solvers/refinement/string_refinement_util.cpp
@@ -36,7 +36,7 @@ bool is_char_type(const typet &type)
 
 bool is_char_array_type(const typet &type, const namespacet &ns)
 {
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
     return is_char_array_type(ns.follow(type), ns);
   return type.id() == ID_array && is_char_type(type.subtype());
 }
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
index f999c4beef7..e26a4225cf1 100644
--- a/src/util/base_type.cpp
+++ b/src/util/base_type.cpp
@@ -53,7 +53,7 @@ class base_type_eqt
 void base_type_rec(
   typet &type, const namespacet &ns, std::set<irep_idt> &symb)
 {
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     const symbolt *symbol;
 
@@ -99,7 +99,7 @@ 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)
+    if(subtype.id() == ID_symbol_type)
     {
       const irep_idt &id = to_symbol_type(subtype).get_identifier();
 
@@ -159,11 +159,10 @@ bool base_type_eqt::base_type_eq_rec(
   #endif
 
   // loop avoidance
-  if((type1.id()==ID_symbol ||
-      type1.id()==ID_c_enum_tag ||
-      type1.id()==ID_struct_tag ||
-      type1.id()==ID_union_tag) &&
-     type2.id()==type1.id())
+  if(
+    (type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
+     type1.id() == ID_struct_tag || type1.id() == ID_union_tag) &&
+    type2.id() == type1.id())
   {
     // already in same set?
     if(identifiers.make_union(
@@ -172,10 +171,9 @@ bool base_type_eqt::base_type_eq_rec(
       return true;
   }
 
-  if(type1.id()==ID_symbol ||
-     type1.id()==ID_c_enum_tag ||
-     type1.id()==ID_struct_tag ||
-     type1.id()==ID_union_tag)
+  if(
+    type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
+    type1.id() == ID_struct_tag || type1.id() == ID_union_tag)
   {
     const symbolt &symbol=
       ns.lookup(type1.get(ID_identifier));
@@ -186,10 +184,9 @@ bool base_type_eqt::base_type_eq_rec(
     return base_type_eq_rec(symbol.type, type2);
   }
 
-  if(type2.id()==ID_symbol ||
-     type2.id()==ID_c_enum_tag ||
-     type2.id()==ID_struct_tag ||
-     type2.id()==ID_union_tag)
+  if(
+    type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag ||
+    type2.id() == ID_struct_tag || type2.id() == ID_union_tag)
   {
     const symbolt &symbol=
       ns.lookup(type2.get(ID_identifier));
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 677f7b6b81e..bd0e54b8a6d 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -51,7 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src)
 
 void endianness_mapt::build_big_endian(const typet &src)
 {
-  if(src.id()==ID_symbol)
+  if(src.id() == ID_symbol_type)
     build_big_endian(ns.follow(src));
   else if(src.id()==ID_c_enum_tag)
     build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 3d8ec337e32..16640b3382b 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -280,7 +280,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
 
     return value;
   }
-  else if(type_id==ID_symbol)
+  else if(type_id == ID_symbol_type)
   {
     exprt result = expr_initializer_rec(ns.follow(type), source_location);
     // we might have mangled the type for arrays, so keep that
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
index 2c6a596ba42..e379120960f 100644
--- a/src/util/find_symbols.cpp
+++ b/src/util/find_symbols.cpp
@@ -165,7 +165,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
       //  dest.insert(identifier);
     }
   }
-  else if(src.id()==ID_symbol)
+  else if(src.id() == ID_symbol_type)
     dest.insert(to_symbol_type(src).get_identifier());
   else if(src.id()==ID_array)
   {
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
index 8d54599598d..1e4bed98ead 100644
--- a/src/util/format_type.cpp
+++ b/src/util/format_type.cpp
@@ -51,7 +51,7 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
   }
   else if(id == ID_struct)
     return format_rec(os, to_struct_type(type));
-  else if(id == ID_symbol)
+  else if(id == ID_symbol_type)
     return os << "symbol_type " << to_symbol_type(type).get_identifier();
   else
     return os << id;
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index d0066054482..95438d3fefd 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -58,6 +58,7 @@ IREP_ID_ONE(bitxnor)
 IREP_ID_ONE(notequal)
 IREP_ID_ONE(if)
 IREP_ID_ONE(symbol)
+IREP_ID_ONE(symbol_type)
 IREP_ID_ONE(next_symbol)
 IREP_ID_ONE(nondet_symbol)
 IREP_ID_ONE(predicate_symbol)
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
index 0e9147fe775..5c30ca16d9d 100644
--- a/src/util/json_expr.cpp
+++ b/src/util/json_expr.cpp
@@ -117,7 +117,7 @@ json_objectt json(
   const namespacet &ns,
   const irep_idt &mode)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return json(ns.follow(type), ns, mode);
 
   json_objectt result;
diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp
index 04a6f260db8..76f0a8dbc40 100644
--- a/src/util/namespace.cpp
+++ b/src/util/namespace.cpp
@@ -60,7 +60,7 @@ const typet &namespace_baset::follow(const typet &src) const
   if(src.id() == ID_struct_tag)
     return follow_tag(to_struct_tag_type(src));
 
-  if(src.id()!=ID_symbol)
+  if(src.id() != ID_symbol_type)
     return src;
 
   const symbolt *symbol = &lookup(to_symbol_type(src));
@@ -70,7 +70,7 @@ const typet &namespace_baset::follow(const typet &src) const
   {
     DATA_INVARIANT(symbol->is_type, "symbol type points to type");
 
-    if(symbol->type.id() == ID_symbol)
+    if(symbol->type.id() == ID_symbol_type)
       symbol = &lookup(to_symbol_type(symbol->type));
     else
       return symbol->type;
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 872e69a65fc..0035ba29fe7 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -234,7 +234,7 @@ mp_integer pointer_offset_bits(
 
     return to_bitvector_type(type).get_width();
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     return pointer_offset_bits(ns.follow(type), ns);
   }
@@ -510,7 +510,7 @@ exprt size_of_expr(
       bytes++;
     return from_integer(bytes, size_type());
   }
-  else if(type.id()==ID_symbol)
+  else if(type.id() == ID_symbol_type)
   {
     return size_of_expr(ns.follow(type), ns);
   }
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
index e568758661f..91acab8de72 100644
--- a/src/util/replace_symbol.cpp
+++ b/src/util/replace_symbol.cpp
@@ -185,7 +185,7 @@ bool replace_symbolt::replace(typet &dest) const
       if(!replace(*it))
         result=false;
   }
-  else if(dest.id()==ID_symbol)
+  else if(dest.id() == ID_symbol_type)
   {
     type_mapt::const_iterator it =
       type_map.find(to_symbol_type(dest).get_identifier());
@@ -250,7 +250,7 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
       if(have_to_replace(*it))
         return true;
   }
-  else if(dest.id()==ID_symbol)
+  else if(dest.id() == ID_symbol_type)
   {
     const irep_idt &identifier = to_symbol_type(dest).get_identifier();
     return type_map.find(identifier) != type_map.end();
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 00f9566926b..39cb1b49b94 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -110,7 +110,7 @@ class real_typet:public typet
 class symbol_typet:public typet
 {
 public:
-  explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol)
+  explicit symbol_typet(const irep_idt &identifier) : typet(ID_symbol_type)
   {
     set_identifier(identifier);
   }
@@ -138,7 +138,7 @@ class symbol_typet:public typet
 */
 inline const symbol_typet &to_symbol_type(const typet &type)
 {
-  PRECONDITION(type.id()==ID_symbol);
+  PRECONDITION(type.id() == ID_symbol_type);
   return static_cast<const symbol_typet &>(type);
 }
 
@@ -147,14 +147,14 @@ inline const symbol_typet &to_symbol_type(const typet &type)
 */
 inline symbol_typet &to_symbol_type(typet &type)
 {
-  PRECONDITION(type.id()==ID_symbol);
+  PRECONDITION(type.id() == ID_symbol_type);
   return static_cast<symbol_typet &>(type);
 }
 
 template <>
 inline bool can_cast_type<symbol_typet>(const typet &type)
 {
-  return type.id() == ID_symbol;
+  return type.id() == ID_symbol_type;
 }
 
 /*! \brief Base type of C structs and unions, and C++ classes
diff --git a/src/util/type.cpp b/src/util/type.cpp
index a83e5576717..2a235c2d652 100644
--- a/src/util/type.cpp
+++ b/src/util/type.cpp
@@ -87,7 +87,7 @@ bool is_constant_or_has_constant_components(
   // we have to use the namespace to resolve to its definition:
   // struct t { const int a; };
   // struct t t1;
-  if(type.id() == ID_symbol)
+  if(type.id() == ID_symbol_type)
   {
     const auto &resolved_type = ns.follow(type);
     return has_constant_components(resolved_type);
diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp
index 5fc587f58e3..5a4e4585d94 100644
--- a/src/util/type_eq.cpp
+++ b/src/util/type_eq.cpp
@@ -20,7 +20,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
   if(type1==type2)
     return true;
 
-  if(type1.id()==ID_symbol)
+  if(type1.id() == ID_symbol_type)
   {
     const symbolt &symbol = ns.lookup(to_symbol_type(type1));
     if(!symbol.is_type)
@@ -29,7 +29,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
     return type_eq(symbol.type, type2, ns);
   }
 
-  if(type2.id()==ID_symbol)
+  if(type2.id() == ID_symbol_type)
   {
     const symbolt &symbol = ns.lookup(to_symbol_type(type2));
     if(!symbol.is_type)
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp
index 319a463b914..56176a88e57 100644
--- a/src/util/xml_expr.cpp
+++ b/src/util/xml_expr.cpp
@@ -51,7 +51,7 @@ xmlt xml(
   const typet &type,
   const namespacet &ns)
 {
-  if(type.id()==ID_symbol)
+  if(type.id() == ID_symbol_type)
     return xml(ns.follow(type), ns);
 
   xmlt result;