diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp
index fa4b7d9c8b2..ccb029d2096 100644
--- a/src/analyses/local_safe_pointers.cpp
+++ b/src/analyses/local_safe_pointers.cpp
@@ -11,6 +11,7 @@ Author: Diffblue Ltd
 
 #include "local_safe_pointers.h"
 
+#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
@@ -81,7 +82,8 @@ static optionalt<goto_null_checkt> get_null_checked_expr(const exprt &expr)
 /// \param goto_program: program to analyse
 void local_safe_pointerst::operator()(const goto_programt &goto_program)
 {
-  std::set<exprt, type_comparet> checked_expressions(type_comparet{});
+  std::set<exprt, base_type_comparet> checked_expressions(
+    base_type_comparet{ns});
 
   for(const auto &instruction : goto_program.instructions)
   {
@@ -96,7 +98,8 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
         checked_expressions = findit->second;
       else
       {
-        checked_expressions = std::set<exprt, type_comparet>(type_comparet{});
+        checked_expressions =
+          std::set<exprt, base_type_comparet>(base_type_comparet{ns});
       }
     }
 
@@ -185,11 +188,8 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
-/// \param ns: namespace
 void local_safe_pointerst::output(
-  std::ostream &out,
-  const goto_programt &goto_program,
-  const namespacet &ns)
+  std::ostream &out, const goto_programt &goto_program)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -229,11 +229,8 @@ void local_safe_pointerst::output(
 /// \param out: stream to write output to
 /// \param goto_program: GOTO program analysed (the same one passed to
 ///   operator())
-/// \param ns: namespace
 void local_safe_pointerst::output_safe_dereferences(
-  std::ostream &out,
-  const goto_programt &goto_program,
-  const namespacet &ns)
+  std::ostream &out, const goto_programt &goto_program)
 {
   forall_goto_program_instructions(i_it, goto_program)
   {
@@ -250,17 +247,12 @@ void local_safe_pointerst::output_safe_dereferences(
       out << "{";
       bool first = true;
       i_it->apply([&first, &out](const exprt &e) {
-        for(auto subexpr_it = e.depth_begin(), subexpr_end = e.depth_end();
-            subexpr_it != subexpr_end;
-            ++subexpr_it)
+        if(e.id() == ID_dereference)
         {
-          if(subexpr_it->id() == ID_dereference)
-          {
-            if(!first)
-              out << ", ";
-            first = true;
-            format_rec(out, to_dereference_expr(*subexpr_it).pointer());
-          }
+          if(!first)
+            out << ", ";
+          first = true;
+          format_rec(out, to_dereference_expr(e).pointer());
         }
       });
       out << "}";
@@ -281,6 +273,17 @@ bool local_safe_pointerst::is_non_null_at_program_point(
   auto findit = non_null_expressions.find(program_point->location_number);
   if(findit == non_null_expressions.end())
     return false;
+  const exprt *tocheck = &expr;
+  while(tocheck->id() == ID_typecast)
+    tocheck = &tocheck->op0();
+  return findit->second.count(*tocheck) != 0;
+}
 
-  return findit->second.count(skip_typecast(expr)) != 0;
+bool local_safe_pointerst::base_type_comparet::operator()(
+  const exprt &e1, const exprt &e2) const
+{
+  if(base_type_eq(e1, e2, ns))
+    return false;
+  else
+    return e1 < e2;
 }
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 041b9b3bf4f..2a1329798f3 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -32,8 +32,6 @@ void c_typecheck_baset::typecheck_code(codet &code)
     throw 0;
   }
 
-  code.type() = empty_typet();
-
   const irep_idt &statement=code.get_statement();
 
   if(statement==ID_expression)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index e99d3a1d136..3579be7f837 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -974,7 +974,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,
@@ -1024,7 +1024,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 672d4616450..679a4c5f2c3 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -195,7 +195,8 @@ std::string expr2ct::convert_rec(
 
   std::string q=new_qualifiers.as_string();
 
-  std::string d = declarator.empty() ? declarator : " " + declarator;
+  std::string d=
+    declarator==""?declarator:" "+declarator;
 
   if(src.find(ID_C_typedef).is_not_nil())
   {
@@ -287,13 +288,13 @@ std::string expr2ct::convert_rec(
     if(width==config.ansi_c.int_width)
     {
       if(is_signed)
-        sign_str.clear();
+        sign_str="";
       return q+sign_str+"int"+d;
     }
     else if(width==config.ansi_c.long_int_width)
     {
       if(is_signed)
-        sign_str.clear();
+        sign_str="";
       return q+sign_str+"long int"+d;
     }
     else if(width==config.ansi_c.char_width)
@@ -304,19 +305,19 @@ std::string expr2ct::convert_rec(
     else if(width==config.ansi_c.short_int_width)
     {
       if(is_signed)
-        sign_str.clear();
+        sign_str="";
       return q+sign_str+"short int"+d;
     }
     else if(width==config.ansi_c.long_long_int_width)
     {
       if(is_signed)
-        sign_str.clear();
+        sign_str="";
       return q+sign_str+"long long int"+d;
     }
     else if(width==128)
     {
       if(is_signed)
-        sign_str.clear();
+        sign_str="";
       return q + sign_str + "__int128" + d;
     }
     else
@@ -336,7 +337,7 @@ std::string expr2ct::convert_rec(
     std::string dest=q+"union";
 
     const irep_idt &tag=union_type.get_tag();
-    if(!tag.empty())
+    if(tag!="")
       dest+=" "+id2string(tag);
 
     if(!union_type.is_incomplete())
@@ -420,7 +421,7 @@ std::string expr2ct::convert_rec(
     // The star gets attached to the declarator.
     std::string new_declarator="*";
 
-    if(!q.empty() && (!declarator.empty() || subtype.id() == ID_pointer))
+    if(q != "" && (!declarator.empty() || subtype.id() == ID_pointer))
     {
       new_declarator+=" "+q;
     }
@@ -448,7 +449,7 @@ std::string expr2ct::convert_rec(
 
     std::string dest=q+"struct";
     const std::string &tag=ns.follow_tag(struct_tag_type).get_string(ID_tag);
-    if(!tag.empty())
+    if(tag!="")
       dest+=" "+tag;
     dest+=d;
 
@@ -461,7 +462,7 @@ std::string expr2ct::convert_rec(
 
     std::string dest=q+"union";
     const std::string &tag=ns.follow_tag(union_tag_type).get_string(ID_tag);
-    if(!tag.empty())
+    if(tag!="")
       dest+=" "+tag;
     dest+=d;
 
@@ -479,7 +480,9 @@ std::string expr2ct::convert_rec(
 
     if(parameters.empty())
     {
-      if(!code_type.has_ellipsis())
+      if(code_type.has_ellipsis())
+        dest+=""; // empty!
+      else
         dest+="void"; // means 'no parameters'
     }
     else
@@ -635,7 +638,7 @@ std::string expr2ct::convert_struct_type(
   std::string dest=qualifiers+"struct";
 
   const irep_idt &tag=struct_type.get_tag();
-  if(!tag.empty())
+  if(tag!="")
     dest+=" "+id2string(tag);
 
   if(inc_struct_body && !struct_type.is_incomplete())
@@ -1157,7 +1160,9 @@ std::string expr2ct::convert_prob_coin(
     return convert_norep(src, precedence);
 }
 
-std::string expr2ct::convert_literal(const exprt &src)
+std::string expr2ct::convert_literal(
+  const exprt &src,
+  unsigned &precedence)
 {
   return "L("+src.get_string(ID_literal)+")";
 }
@@ -1173,20 +1178,34 @@ std::string expr2ct::convert_prob_uniform(
     return convert_norep(src, precedence);
 }
 
-std::string expr2ct::convert_function(const exprt &src, const std::string &name)
+std::string expr2ct::convert_function(
+  const exprt &src,
+  const std::string &name,
+  unsigned precedence)
+{
+  return convert_function(src.operands(), name, precedence);
+}
+
+std::string expr2ct::convert_function(
+  const exprt::operandst &ops,
+  const std::string &name,
+  unsigned precedence)
 {
   std::string dest=name;
   dest+='(';
+  bool first = true;
 
-  forall_operands(it, src)
+  for(const auto &op : ops)
   {
     unsigned p;
-    std::string op=convert_with_precedence(*it, p);
+    const std::string op_str=convert_with_precedence(op, p);
 
-    if(it!=src.operands().begin())
+    if(first)
+      first=false;
+    else
       dest+=", ";
 
-    dest+=op;
+    dest+=op_str;
   }
 
   dest+=')';
@@ -1518,7 +1537,7 @@ std::string expr2ct::convert_member(
 
   irep_idt component_name=src.get_component_name();
 
-  if(!component_name.empty())
+  if(component_name!="")
   {
     const exprt &comp_expr = struct_union_type.get_component(component_name);
 
@@ -1566,7 +1585,7 @@ std::string expr2ct::convert_struct_member_value(
 }
 
 std::string expr2ct::convert_norep(
-  const exprt &src,
+  const irept &src,
   unsigned &precedence)
 {
   lispexprt lisp;
@@ -1576,7 +1595,9 @@ std::string expr2ct::convert_norep(
   return dest;
 }
 
-std::string expr2ct::convert_symbol(const exprt &src)
+std::string expr2ct::convert_symbol(
+  const exprt &src,
+  unsigned &precedence)
 {
   const irep_idt &id=src.get(ID_identifier);
   std::string dest;
@@ -1616,37 +1637,49 @@ std::string expr2ct::convert_symbol(const exprt &src)
   return dest;
 }
 
-std::string expr2ct::convert_nondet_symbol(const nondet_symbol_exprt &src)
+std::string expr2ct::convert_nondet_symbol(
+  const nondet_symbol_exprt &src,
+  unsigned &precedence)
 {
   const irep_idt id=src.get_identifier();
   return "nondet_symbol("+id2string(id)+")";
 }
 
-std::string expr2ct::convert_predicate_symbol(const exprt &src)
+std::string expr2ct::convert_predicate_symbol(
+  const exprt &src,
+  unsigned &precedence)
 {
   const std::string &id=src.get_string(ID_identifier);
   return "ps("+id+")";
 }
 
-std::string expr2ct::convert_predicate_next_symbol(const exprt &src)
+std::string expr2ct::convert_predicate_next_symbol(
+  const exprt &src,
+  unsigned &precedence)
 {
   const std::string &id=src.get_string(ID_identifier);
   return "pns("+id+")";
 }
 
-std::string expr2ct::convert_predicate_passive_symbol(const exprt &src)
+std::string expr2ct::convert_predicate_passive_symbol(
+  const exprt &src,
+  unsigned &precedence)
 {
   const std::string &id=src.get_string(ID_identifier);
   return "pps("+id+")";
 }
 
-std::string expr2ct::convert_quantified_symbol(const exprt &src)
+std::string expr2ct::convert_quantified_symbol(
+  const exprt &src,
+  unsigned &precedence)
 {
   const std::string &id=src.get_string(ID_identifier);
   return id;
 }
 
-std::string expr2ct::convert_nondet_bool()
+std::string expr2ct::convert_nondet_bool(
+  const exprt &src,
+  unsigned &precedence)
 {
   return "nondet_bool()";
 }
@@ -1813,7 +1846,7 @@ std::string expr2ct::convert_constant(
   {
     dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
 
-    if(!dest.empty() && isdigit(dest[dest.size() - 1]))
+    if(dest!="" && isdigit(dest[dest.size()-1]))
     {
       if(dest.find('.')==std::string::npos)
         dest+=".0";
@@ -1867,7 +1900,7 @@ std::string expr2ct::convert_constant(
   {
     dest=fixedbvt(to_constant_expr(src)).to_ansi_c_string();
 
-    if(!dest.empty() && isdigit(dest[dest.size() - 1]))
+    if(dest!="" && isdigit(dest[dest.size()-1]))
     {
       if(src.type()==float_type())
         dest+='f';
@@ -1877,7 +1910,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id() == ID_array)
   {
-    dest = convert_array(src);
+    dest=convert_array(src, precedence);
   }
   else if(type.id()==ID_pointer)
   {
@@ -2094,7 +2127,9 @@ std::string expr2ct::convert_union(
   return dest;
 }
 
-std::string expr2ct::convert_array(const exprt &src)
+std::string expr2ct::convert_array(
+  const exprt &src,
+  unsigned &precedence)
 {
   std::string dest;
 
@@ -2229,7 +2264,9 @@ std::string expr2ct::convert_array_list(
   return dest;
 }
 
-std::string expr2ct::convert_initializer_list(const exprt &src)
+std::string expr2ct::convert_initializer_list(
+  const exprt &src,
+  unsigned &precedence)
 {
   std::string dest;
   if(src.id()!=ID_compound_literal)
@@ -2255,7 +2292,9 @@ std::string expr2ct::convert_initializer_list(const exprt &src)
   return dest;
 }
 
-std::string expr2ct::convert_designated_initializer(const exprt &src)
+std::string expr2ct::convert_designated_initializer(
+  const exprt &src,
+  unsigned &precedence)
 {
   if(src.operands().size()!=1)
   {
@@ -2271,8 +2310,9 @@ std::string expr2ct::convert_designated_initializer(const exprt &src)
   return dest;
 }
 
-std::string
-expr2ct::convert_function_application(const function_application_exprt &src)
+std::string expr2ct::convert_function_application(
+  const function_application_exprt &src,
+  unsigned &precedence)
 {
   std::string dest;
 
@@ -2301,7 +2341,8 @@ expr2ct::convert_function_application(const function_application_exprt &src)
 }
 
 std::string expr2ct::convert_side_effect_expr_function_call(
-  const side_effect_expr_function_callt &src)
+  const side_effect_expr_function_callt &src,
+  unsigned &precedence)
 {
   std::string dest;
 
@@ -2568,7 +2609,9 @@ std::string expr2ct::convert_code_goto(
   return dest;
 }
 
-std::string expr2ct::convert_code_break(unsigned indent)
+std::string expr2ct::convert_code_break(
+  const codet &src,
+  unsigned indent)
 {
   std::string dest=indent_str(indent);
   dest+="break";
@@ -2620,7 +2663,9 @@ std::string expr2ct::convert_code_switch(
   return dest;
 }
 
-std::string expr2ct::convert_code_continue(unsigned indent)
+std::string expr2ct::convert_code_continue(
+  const codet &src,
+  unsigned indent)
 {
   std::string dest=indent_str(indent);
   dest+="continue";
@@ -2875,10 +2920,10 @@ std::string expr2ct::convert_code(
     return convert_code_assert(src, indent);
 
   if(statement==ID_break)
-    return convert_code_break(indent);
+    return convert_code_break(src, indent);
 
   if(statement==ID_continue)
-    return convert_code_continue(indent);
+    return convert_code_continue(src, indent);
 
   if(statement==ID_decl)
     return convert_code_decl(src, indent);
@@ -2923,7 +2968,7 @@ std::string expr2ct::convert_code(
     return convert_code_array_replace(src, indent);
 
   if(statement == ID_set_may || statement == ID_set_must)
-    return indent_str(indent) + convert_function(src, id2string(statement)) +
+    return indent_str(indent) + convert_function(src, id2string(statement), 16) +
            ";";
 
   unsigned precedence;
@@ -2934,7 +2979,15 @@ std::string expr2ct::convert_code_assign(
   const code_assignt &src,
   unsigned indent)
 {
-  std::string tmp=convert_binary(src, "=", 2, true);
+  if(src.operands().size()!=2)
+  {
+    unsigned precedence;
+    return convert_norep(src, precedence);
+  }
+
+  binary_exprt tmp_binary(src.lhs(), ID_assign, src.rhs());
+
+  std::string tmp=convert_binary(tmp_binary, "=", 2, true);
 
   std::string dest=indent_str(indent)+tmp+";";
 
@@ -3359,22 +3412,23 @@ std::string expr2ct::convert_with_precedence(
     return convert_unary(to_unary_expr(src), "+", precedence = 15);
 
   else if(src.id()==ID_floatbv_plus)
-    return convert_function(src, "FLOAT+");
+    return convert_function(src, "FLOAT+", precedence=16);
 
   else if(src.id()==ID_floatbv_minus)
-    return convert_function(src, "FLOAT-");
+    return convert_function(src, "FLOAT-", precedence=16);
 
   else if(src.id()==ID_floatbv_mult)
-    return convert_function(src, "FLOAT*");
+    return convert_function(src, "FLOAT*", precedence=16);
 
   else if(src.id()==ID_floatbv_div)
-    return convert_function(src, "FLOAT/");
+    return convert_function(src, "FLOAT/", precedence=16);
 
   else if(src.id()==ID_floatbv_rem)
-    return convert_function(src, "FLOAT%");
+    return convert_function(src, "FLOAT%", precedence=16);
 
   else if(src.id()==ID_floatbv_typecast)
   {
+    precedence=16;
     std::string dest="FLOAT_TYPECAST(";
 
     unsigned p0;
@@ -3407,33 +3461,33 @@ std::string expr2ct::convert_with_precedence(
   {
     if(src.operands().size()==1 &&
        src.op0().type().id()==ID_floatbv)
-      return convert_function(src, "signbit");
+      return convert_function(src, "signbit", precedence=16);
     else
-      return convert_function(src, "SIGN");
+      return convert_function(src, "SIGN", precedence=16);
   }
 
   else if(src.id()==ID_popcount)
   {
     if(config.ansi_c.mode==configt::ansi_ct::flavourt::VISUAL_STUDIO)
-      return convert_function(src, "__popcnt");
+      return convert_function(src, "__popcnt", precedence=16);
     else
-      return convert_function(src, "__builtin_popcount");
+      return convert_function(src, "__builtin_popcount", precedence=16);
   }
 
   else if(src.id() == ID_r_ok)
-    return convert_function(src, "R_OK");
+    return convert_function(src, "R_OK", precedence = 16);
 
   else if(src.id() == ID_w_ok)
-    return convert_function(src, "W_OK");
+    return convert_function(src, "W_OK", precedence = 16);
 
   else if(src.id() == ID_is_invalid_pointer)
-    return convert_function(src, "IS_INVALID_POINTER");
+    return convert_function(src, "IS_INVALID_POINTER", precedence = 16);
 
   else if(src.id()==ID_good_pointer)
-    return convert_function(src, "GOOD_POINTER");
+    return convert_function(src, "GOOD_POINTER", precedence=16);
 
   else if(src.id()==ID_object_size)
-    return convert_function(src, "OBJECT_SIZE");
+    return convert_function(src, "OBJECT_SIZE", precedence=16);
 
   else if(src.id()=="pointer_arithmetic")
     return convert_pointer_arithmetic(src, precedence=16);
@@ -3453,83 +3507,85 @@ std::string expr2ct::convert_with_precedence(
   }
 
   else if(src.id()==ID_infinity)
-    return convert_function(src, "INFINITY");
+    return convert_function(src, "INFINITY", precedence=16);
 
   else if(src.id()=="builtin-function")
     return src.get_string(ID_identifier);
 
   else if(src.id()==ID_pointer_object)
-    return convert_function(src, "POINTER_OBJECT");
+    return convert_function(src, "POINTER_OBJECT", precedence=16);
 
   else if(src.id() == ID_get_must)
-    return convert_function(src, CPROVER_PREFIX "get_must");
+    return convert_function(src, CPROVER_PREFIX "get_must", precedence=16);
 
   else if(src.id() == ID_get_may)
-    return convert_function(src, CPROVER_PREFIX "get_may");
+    return convert_function(src, CPROVER_PREFIX "get_may", precedence=16);
 
   else if(src.id()=="object_value")
-    return convert_function(src, "OBJECT_VALUE");
+    return convert_function(src, "OBJECT_VALUE", precedence=16);
 
   else if(src.id()==ID_array_of)
     return convert_array_of(src, precedence=16);
 
   else if(src.id()==ID_pointer_offset)
-    return convert_function(src, "POINTER_OFFSET");
+    return convert_function(src, "POINTER_OFFSET", precedence=16);
 
   else if(src.id()=="pointer_base")
-    return convert_function(src, "POINTER_BASE");
+    return convert_function(src, "POINTER_BASE", precedence=16);
 
   else if(src.id()=="pointer_cons")
-    return convert_function(src, "POINTER_CONS");
+    return convert_function(src, "POINTER_CONS", precedence=16);
 
   else if(src.id() == ID_is_invalid_pointer)
-    return convert_function(src, CPROVER_PREFIX "is_invalid_pointer");
+    return convert_function(
+      src, CPROVER_PREFIX "is_invalid_pointer", precedence = 16);
 
   else if(src.id() == ID_dynamic_object)
-    return convert_function(src, "DYNAMIC_OBJECT");
+    return convert_function(src, "DYNAMIC_OBJECT", precedence = 16);
 
   else if(src.id() == ID_is_dynamic_object)
-    return convert_function(src, "IS_DYNAMIC_OBJECT");
+    return convert_function(src, "IS_DYNAMIC_OBJECT", precedence = 16);
 
   else if(src.id()=="is_zero_string")
-    return convert_function(src, "IS_ZERO_STRING");
+    return convert_function(src, "IS_ZERO_STRING", precedence=16);
 
   else if(src.id()=="zero_string")
-    return convert_function(src, "ZERO_STRING");
+    return convert_function(src, "ZERO_STRING", precedence=16);
 
   else if(src.id()=="zero_string_length")
-    return convert_function(src, "ZERO_STRING_LENGTH");
+    return convert_function(src, "ZERO_STRING_LENGTH", precedence=16);
 
   else if(src.id()=="buffer_size")
-    return convert_function(src, "BUFFER_SIZE");
+    return convert_function(src, "BUFFER_SIZE", precedence=16);
 
   else if(src.id()==ID_isnan)
-    return convert_function(src, "isnan");
+    return convert_function(src, "isnan", precedence=16);
 
   else if(src.id()==ID_isfinite)
-    return convert_function(src, "isfinite");
+    return convert_function(src, "isfinite", precedence=16);
 
   else if(src.id()==ID_isinf)
-    return convert_function(src, "isinf");
+    return convert_function(src, "isinf", precedence=16);
 
   else if(src.id()==ID_bswap)
     return convert_function(
       src,
       "__builtin_bswap" +
-        integer2string(*pointer_offset_bits(src.op0().type(), ns)));
+        integer2string(*pointer_offset_bits(src.op0().type(), ns)),
+      precedence = 16);
 
   else if(src.id()==ID_isnormal)
-    return convert_function(src, "isnormal");
+    return convert_function(src, "isnormal", precedence=16);
 
   else if(src.id()==ID_builtin_offsetof)
-    return convert_function(src, "builtin_offsetof");
+    return convert_function(src, "builtin_offsetof", precedence=16);
 
   else if(src.id()==ID_gcc_builtin_va_arg)
-    return convert_function(src, "gcc_builtin_va_arg");
+    return convert_function(src, "gcc_builtin_va_arg", precedence=16);
 
   else if(src.id()==ID_alignof)
     // C uses "_Alignof", C++ uses "alignof"
-    return convert_function(src, "alignof");
+    return convert_function(src, "alignof", precedence=16);
 
   else if(has_prefix(src.id_string(), "byte_extract"))
     return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
@@ -3582,7 +3638,9 @@ std::string expr2ct::convert_with_precedence(
     return convert_struct_member_value(src, precedence=16);
 
   else if(src.id()==ID_function_application)
-    return convert_function_application(to_function_application_expr(src));
+    return
+      convert_function_application(
+        to_function_application_expr(src), precedence);
 
   else if(src.id()==ID_side_effect)
   {
@@ -3618,12 +3676,13 @@ std::string expr2ct::convert_with_precedence(
     else if(statement==ID_assign)
       return convert_binary(src, "=", precedence=2, true);
     else if(statement==ID_function_call)
-      return convert_side_effect_expr_function_call(
-        to_side_effect_expr_function_call(src));
+      return
+        convert_side_effect_expr_function_call(
+          to_side_effect_expr_function_call(src), precedence);
     else if(statement == ID_allocate)
       return convert_allocate(src, precedence = 15);
     else if(statement==ID_printf)
-      return convert_function(src, "printf");
+      return convert_function(src, "printf", precedence=16);
     else if(statement==ID_nondet)
       return convert_nondet(src, precedence=16);
     else if(statement=="prob_coin")
@@ -3633,13 +3692,13 @@ std::string expr2ct::convert_with_precedence(
     else if(statement==ID_statement_expression)
       return convert_statement_expression(src, precedence=15);
     else if(statement == ID_va_start)
-      return convert_function(src, CPROVER_PREFIX "va_start");
+      return convert_function(src, CPROVER_PREFIX "va_start", precedence=16);
     else
       return convert_norep(src, precedence);
   }
 
   else if(src.id()==ID_literal)
-    return convert_literal(src);
+    return convert_literal(src, precedence=16);
 
   else if(src.id()==ID_not)
     return convert_unary(to_unary_expr(src), "!", precedence = 15);
@@ -3673,25 +3732,25 @@ std::string expr2ct::convert_with_precedence(
     return convert_binary(src, "==", precedence=9, true);
 
   else if(src.id()==ID_ieee_float_equal)
-    return convert_function(src, "IEEE_FLOAT_EQUAL");
+    return convert_function(src, "IEEE_FLOAT_EQUAL", precedence=16);
 
   else if(src.id()==ID_width)
-    return convert_function(src, "WIDTH");
+    return convert_function(src, "WIDTH", precedence=16);
 
   else if(src.id()==ID_concatenation)
-    return convert_function(src, "CONCATENATION");
+    return convert_function(src, "CONCATENATION", precedence=16);
 
   else if(src.id()==ID_ieee_float_notequal)
-    return convert_function(src, "IEEE_FLOAT_NOTEQUAL");
+    return convert_function(src, "IEEE_FLOAT_NOTEQUAL", precedence=16);
 
   else if(src.id()==ID_abs)
-    return convert_function(src, "abs");
+    return convert_function(src, "abs", precedence=16);
 
   else if(src.id()==ID_complex_real)
-    return convert_function(src, "__real__");
+    return convert_function(src, "__real__", precedence=16);
 
   else if(src.id()==ID_complex_imag)
-    return convert_function(src, "__imag__");
+    return convert_function(src, "__imag__", precedence=16);
 
   else if(src.id()==ID_complex)
     return convert_complex(src, precedence=16);
@@ -3745,28 +3804,28 @@ std::string expr2ct::convert_with_precedence(
     return precedence=16, convert_index_designator(src);
 
   else if(src.id()==ID_symbol)
-    return convert_symbol(src);
+    return convert_symbol(src, precedence);
 
   else if(src.id()==ID_next_symbol)
-    return convert_symbol(src);
+    return convert_symbol(src, precedence);
 
   else if(src.id()==ID_nondet_symbol)
-    return convert_nondet_symbol(to_nondet_symbol_expr(src));
+    return convert_nondet_symbol(to_nondet_symbol_expr(src), precedence);
 
   else if(src.id()==ID_predicate_symbol)
-    return convert_predicate_symbol(src);
+    return convert_predicate_symbol(src, precedence);
 
   else if(src.id()==ID_predicate_next_symbol)
-    return convert_predicate_next_symbol(src);
+    return convert_predicate_next_symbol(src, precedence);
 
   else if(src.id()==ID_predicate_passive_symbol)
-    return convert_predicate_passive_symbol(src);
+    return convert_predicate_passive_symbol(src, precedence);
 
   else if(src.id()=="quant_symbol")
-    return convert_quantified_symbol(src);
+    return convert_quantified_symbol(src, precedence);
 
   else if(src.id()==ID_nondet_bool)
-    return convert_nondet_bool();
+    return convert_nondet_bool(src, precedence);
 
   else if(src.id()==ID_object_descriptor)
     return convert_object_descriptor(src, precedence);
@@ -3794,7 +3853,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_union(to_unary_expr(src), precedence);
 
   else if(src.id()==ID_array)
-    return convert_array(src);
+    return convert_array(src, precedence);
 
   else if(src.id() == ID_array_list)
     return convert_array_list(src, precedence);
@@ -3833,16 +3892,10 @@ std::string expr2ct::convert_with_precedence(
 
   else if(src.id()==ID_initializer_list ||
           src.id()==ID_compound_literal)
-  {
-    precedence = 15;
-    return convert_initializer_list(src);
-  }
+    return convert_initializer_list(src, precedence=15);
 
   else if(src.id()==ID_designated_initializer)
-  {
-    precedence = 15;
-    return convert_designated_initializer(src);
-  }
+    return convert_designated_initializer(src, precedence=15);
 
   else if(src.id()==ID_sizeof)
     return convert_sizeof(src, precedence);
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index a28502504e7..2ce009ba090 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -169,7 +169,15 @@ class expr2ct
     const exprt &src, const std::string &symbol,
     unsigned precedence);
 
-  std::string convert_function(const exprt &src, const std::string &symbol);
+  std::string convert_function(
+    const exprt::operandst &ops,
+    const std::string &symbol,
+    unsigned precedence);
+
+  std::string convert_function(
+    const exprt &src,
+    const std::string &symbol,
+    unsigned precedence);
 
   std::string convert_complex(
     const exprt &src,
@@ -199,9 +207,9 @@ class expr2ct
   std::string convert_code_goto(const codet &src, unsigned indent);
   std::string convert_code_assume(const codet &src, unsigned indent);
   std::string convert_code_assert(const codet &src, unsigned indent);
-  std::string convert_code_break(unsigned indent);
+  std::string convert_code_break(const codet &src, unsigned indent);
   std::string convert_code_switch(const codet &src, unsigned indent);
-  std::string convert_code_continue(unsigned indent);
+  std::string convert_code_continue(const codet &src, unsigned indent);
   std::string convert_code_decl(const codet &src, unsigned indent);
   std::string convert_code_decl_block(const codet &src, unsigned indent);
   std::string convert_code_dead(const codet &src, unsigned indent);
@@ -220,10 +228,10 @@ class expr2ct
   virtual std::string convert_with_precedence(
     const exprt &src, unsigned &precedence);
 
-  std::string
-  convert_function_application(const function_application_exprt &src);
-  std::string convert_side_effect_expr_function_call(
-    const side_effect_expr_function_callt &src);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
   std::string convert_allocate(const exprt &src, unsigned &precedence);
   std::string convert_nondet(const exprt &src, unsigned &precedence);
   std::string convert_prob_coin(const exprt &src, unsigned &precedence);
@@ -231,28 +239,32 @@ class expr2ct
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_statement_expression(const exprt &src, unsigned &precendence);
 
-  virtual std::string convert_symbol(const exprt &src);
-  std::string convert_predicate_symbol(const exprt &src);
-  std::string convert_predicate_next_symbol(const exprt &src);
-  std::string convert_predicate_passive_symbol(const exprt &src);
-  std::string convert_nondet_symbol(const nondet_symbol_exprt &);
-  std::string convert_quantified_symbol(const exprt &src);
-  std::string convert_nondet_bool();
+  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
+  std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence);
+  std::string convert_quantified_symbol(const exprt &src, unsigned &precedence);
+  std::string convert_nondet_bool(const exprt &src, unsigned &precedence);
   std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
-  std::string convert_literal(const exprt &src);
+  std::string convert_literal(const exprt &src, unsigned &precedence);
   // NOLINTNEXTLINE(whitespace/line_length)
   virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
   virtual std::string convert_constant_bool(bool boolean_value);
 
-  std::string convert_norep(const exprt &src, unsigned &precedence);
+  std::string convert_norep(const irept &src, unsigned &precedence);
 
   virtual std::string convert_struct(const exprt &src, unsigned &precedence);
   std::string convert_union(const exprt &src, unsigned &precedence);
   std::string convert_vector(const exprt &src, unsigned &precedence);
-  std::string convert_array(const exprt &src);
+  std::string convert_array(const exprt &src, unsigned &precedence);
   std::string convert_array_list(const exprt &src, unsigned &precedence);
-  std::string convert_initializer_list(const exprt &src);
-  std::string convert_designated_initializer(const exprt &src);
+  std::string convert_initializer_list(const exprt &src, unsigned &precedence);
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
   std::string convert_concatenation(const exprt &src, unsigned &precedence);
   std::string convert_sizeof(const exprt &src, unsigned &precedence);
   std::string convert_let(const let_exprt &, unsigned precedence);
diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp
index f1b985bc1f0..59d2359d1c3 100644
--- a/src/cpp/cpp_destructor.cpp
+++ b/src/cpp/cpp_destructor.cpp
@@ -64,7 +64,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
 
       auto i_code = cpp_destructor(source_location, index);
       if(i_code.has_value())
-        new_code.add_to_operands(std::move(i_code.value()));
+        new_code.add(std::move(i_code.value()));
     }
 
     return std::move(new_code);
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index cc4144682aa..3eb3f6bf37e 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -26,12 +26,10 @@ void cpp_typecheckt::typecheck_code(codet &code)
 
   if(statement==ID_try_catch)
   {
-    code.type() = empty_typet();
     typecheck_try_catch(code);
   }
   else if(statement==ID_member_initializer)
   {
-    code.type() = empty_typet();
     typecheck_member_initializer(code);
   }
   else if(statement==ID_msc_if_exists ||
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index d642c56e322..04b2246bb73 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -47,7 +47,7 @@ static void copy_parent(
   code_assignt code(dereference_exprt(op0), op1);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code to copy the member.
@@ -76,7 +76,7 @@ static void copy_member(
   code_expressiont code(assign);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code to copy the member.
@@ -113,7 +113,7 @@ static void copy_array(
   code_expressiont code(assign);
   code.add_source_location() = source_location;
 
-  block.operands().push_back(code);
+  block.operands().push_back(code.as_expr());
 }
 
 /// Generate code for implicit default constructors
@@ -580,6 +580,7 @@ void cpp_typecheckt::full_member_initialization(
 
       code_ifthenelset cond(
         cpp_namet("@most_derived").as_expr(), std::move(block));
+
       final_initializers.move_to_sub(cond);
     }
 
diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp
index 5fbbe3ea60c..c6ca573f798 100644
--- a/src/cpp/cpp_typecheck_declaration.cpp
+++ b/src/cpp/cpp_typecheck_declaration.cpp
@@ -171,7 +171,7 @@ void cpp_typecheckt::convert_non_template_declaration(
         declarator.init_args().operands());
 
       if(constructor.has_value())
-        symbol.value = constructor.value();
+        symbol.value = constructor.value().as_expr();
       else
         symbol.value = nil_exprt();
     }
diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp
index 3ea088bb419..d9a8f18193c 100644
--- a/src/cpp/cpp_typecheck_function.cpp
+++ b/src/cpp/cpp_typecheck_function.cpp
@@ -31,7 +31,6 @@ void cpp_typecheckt::convert_parameter(
     parameter.set_base_name(base_name);
   }
 
-  PRECONDITION(!cpp_scopes.current_scope().prefix.empty());
   irep_idt identifier=cpp_scopes.current_scope().prefix+
                       id2string(base_name);
 
@@ -42,7 +41,7 @@ void cpp_typecheckt::convert_parameter(
   if(!lookup(identifier, check_symbol))
     return;
 
-  parameter_symbolt symbol;
+  symbolt symbol;
 
   symbol.name=identifier;
   symbol.base_name=parameter.get_base_name();
@@ -50,7 +49,9 @@ void cpp_typecheckt::convert_parameter(
   symbol.mode = current_mode;
   symbol.module=module;
   symbol.type=parameter.type();
+  symbol.is_state_var=true;
   symbol.is_lvalue=!is_reference(symbol.type);
+  symbol.is_parameter=true;
 
   INVARIANT(!symbol.base_name.empty(), "parameter has base name");
 
@@ -91,6 +92,22 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   if(symbol.value.is_nil())
     return;
 
+  // if it is a destructor, add the implicit code
+  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
+  {
+    const symbolt &msymb=lookup(symbol.type.get(ID_C_member_name));
+
+    assert(symbol.value.id()==ID_code);
+    assert(symbol.value.get(ID_statement)==ID_block);
+
+    if(
+      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
+      symbol.value.op0().op0().id() != ID_already_typechecked)
+    {
+      symbol.value.copy_to_operands(dtor(msymb).as_expr());
+    }
+  }
+
   // enter appropriate scope
   cpp_save_scopet saved_scope(cpp_scopes);
   cpp_scopet &function_scope=cpp_scopes.set_scope(symbol.name);
@@ -108,29 +125,13 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
     code_typet::parameterst &parameters=function_type.parameters();
     assert(parameters.size()>=1);
     code_typet::parametert &this_parameter_expr=parameters.front();
-    function_scope.this_expr = symbol_exprt{
-      this_parameter_expr.get_identifier(), this_parameter_expr.type()};
+    function_scope.this_expr=exprt(ID_symbol, this_parameter_expr.type());
+    function_scope.this_expr.set(
+      ID_identifier, this_parameter_expr.get_identifier());
   }
   else
     function_scope.this_expr.make_nil();
 
-  // if it is a destructor, add the implicit code
-  if(to_code_type(symbol.type).return_type().id() == ID_destructor)
-  {
-    const symbolt &msymb = lookup(symbol.type.get(ID_C_member_name));
-
-    PRECONDITION(symbol.value.id() == ID_code);
-    PRECONDITION(symbol.value.get(ID_statement) == ID_block);
-
-    if(
-      !symbol.value.has_operands() || !symbol.value.op0().has_operands() ||
-      symbol.value.op0().op0().id() != ID_already_typechecked)
-    {
-      symbol.value.copy_to_operands(
-        dtor(msymb, to_symbol_expr(function_scope.this_expr)));
-    }
-  }
-
   // do the function body
   start_typecheck_code();
 
@@ -148,8 +149,6 @@ void cpp_typecheckt::convert_function(symbolt &symbol)
   symbol.value.type()=symbol.type;
 
   return_type = old_return_type;
-
-  deferred_typechecking.erase(symbol.name);
 }
 
 /// for function overloading
@@ -174,7 +173,8 @@ irep_idt cpp_typecheckt::function_identifier(const typet &type)
   code_typet::parameterst::const_iterator it=
     parameters.begin();
 
-  if(it != parameters.end() && it->get_this())
+  if(it!=parameters.end() &&
+     it->get_identifier()==ID_this)
   {
     const typet &pointer=it->type();
     const typet &symbol =pointer.subtype();
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 8ab4510a7ba..8f9543f180d 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -178,7 +178,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol)
       cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
 
     if(constructor.has_value())
-      symbol.value = constructor.value();
+      symbol.value = constructor.value().as_expr();
     else
       symbol.value = nil_exprt();
   }
@@ -307,7 +307,7 @@ void cpp_typecheckt::zero_initializer(
     already_typechecked_exprt::make_already_typechecked(assign.lhs());
 
     typecheck_code(assign);
-    ops.push_back(assign);
+    ops.push_back(assign.as_expr());
   }
   else
   {
@@ -328,6 +328,6 @@ void cpp_typecheckt::zero_initializer(
     already_typechecked_exprt::make_already_typechecked(assign.lhs());
 
     typecheck_code(assign);
-    ops.push_back(assign);
+    ops.push_back(assign.as_expr());
   }
 }
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
index cba5bb227f8..ac76c1d8879 100644
--- a/src/cpp/expr2cpp.cpp
+++ b/src/cpp/expr2cpp.cpp
@@ -461,15 +461,15 @@ std::string expr2cppt::convert_code(
   const codet &src,
   unsigned indent)
 {
-  const irep_idt &statement=src.get(ID_statement);
+  const irep_idt &statement = src.get_statement();
 
   if(statement==ID_cpp_delete ||
      statement==ID_cpp_delete_array)
-    return convert_code_cpp_delete(src, indent);
+    return convert_code_cpp_delete(src.as_expr(), indent);
 
   if(statement==ID_cpp_new ||
      statement==ID_cpp_new_array)
-    return convert_code_cpp_new(src, indent);
+    return convert_cpp_new(src.as_expr(), indent);
 
   return expr2ct::convert_code(src, indent);
 }
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index b869257466d..b0dc9289a96 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -2711,7 +2711,7 @@ bool Parser::rConstructorDecl(
     {
     case TOK_INTEGER:
       {
-        constructor.value()=codet("cpp-pure-virtual");
+        constructor.value() = exprt("cpp-pure-virtual");
         set_location(constructor.value(), value);
       }
       break;
@@ -2724,7 +2724,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_default);
+        constructor.value() = exprt(ID_default);
         set_location(constructor.value(), value);
       }
       break;
@@ -2737,7 +2737,7 @@ bool Parser::rConstructorDecl(
           return false;
         }
 
-        constructor.value()=codet(ID_cpp_delete);
+        constructor.value() = exprt(ID_cpp_delete);
         set_location(constructor.value(), value);
       }
       break;
@@ -2902,7 +2902,7 @@ bool Parser::rDeclaratorWithInit(
         }
 
         lex.get_token(tk);
-        declarator.value()=codet(ID_default);
+        declarator.value() = exprt(ID_default);
         set_location(declarator.value(), tk);
       }
       else if(lex.LookAhead(0)==TOK_DELETE) // C++0x
@@ -2914,7 +2914,7 @@ bool Parser::rDeclaratorWithInit(
         }
 
         lex.get_token(tk);
-        declarator.value()=codet(ID_cpp_delete);
+        declarator.value() = exprt(ID_cpp_delete);
         set_location(declarator.value(), tk);
       }
       else
@@ -3412,7 +3412,7 @@ bool Parser::rMemberInit(exprt &init)
   std::cout << std::string(__indent, ' ') << "Parser::rMemberInit 2\n";
 #endif
 
-  init=codet(ID_member_initializer);
+  init = exprt(ID_member_initializer);
   init.add(ID_member).swap(name);
 
   cpp_tokent tk1, tk2;
@@ -7186,7 +7186,7 @@ bool Parser::rFunctionBody(cpp_declaratort &declarator)
     if(lex.get_token(cb)!='}')
       return false;
 
-    declarator.value()=body;
+    declarator.value() = body.as_expr();
     return true;
   }
   else
diff --git a/src/goto-programs/compute_called_functions.cpp b/src/goto-programs/compute_called_functions.cpp
index 0e1f73f6562..38bdd817ea6 100644
--- a/src/goto-programs/compute_called_functions.cpp
+++ b/src/goto-programs/compute_called_functions.cpp
@@ -55,11 +55,9 @@ void compute_address_taken_functions(
   std::unordered_set<irep_idt> &address_taken)
 {
   for(const auto &i : goto_program.instructions)
-  {
     i.apply([&address_taken](const exprt &expr) {
       compute_address_taken_functions(expr, address_taken);
     });
-  }
 }
 
 /// get all functions whose address is taken
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index faa81d23721..936167567b5 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -526,7 +526,7 @@ void goto_convertt::remove_statement_expression(
     exprt e=to_code_assign(last).lhs();
     code_assignt assignment(tmp_symbol_expr, e);
     assignment.add_source_location()=source_location;
-    code.operands().push_back(assignment);
+    to_code_block(code).add(std::move(assignment));
   }
   else
   {
diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp
index 968eb8186d5..6af8219fd79 100644
--- a/src/goto-programs/rewrite_union.cpp
+++ b/src/goto-programs/rewrite_union.cpp
@@ -101,17 +101,16 @@ void rewrite_union(exprt &expr)
 
 void rewrite_union(goto_functionst::goto_functiont &goto_function)
 {
-  Forall_goto_program_instructions(it, goto_function.body)
-  {
-    rewrite_union(it->code);
-
-    if(it->has_condition())
-    {
-      exprt c = it->get_condition();
-      rewrite_union(c);
-      it->set_condition(c);
-    }
-  }
+  for(auto &instruction : goto_function.body.instructions)
+    instruction.transform([](exprt src) -> optionalt<exprt> {
+      if(!have_to_rewrite_union(src))
+        return {};
+      else
+      {
+        rewrite_union(src);
+        return src;
+      }
+    });
 }
 
 void rewrite_union(goto_functionst &goto_functions)
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 364a83b4376..072a7f0b34b 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -17,7 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/abstract_goto_model.h>
 
+#include "goto_symex_state.h"
 #include "path_storage.h"
+#include "symex_target_equation.h"
 
 class byte_extract_exprt;
 class function_application_exprt;
@@ -37,31 +39,21 @@ class side_effect_exprt;
 class symex_assignt;
 class typecast_exprt;
 
-/// Configuration used for a symbolic execution
+/// Configuration of the symbolic execution
 struct symex_configt final
 {
-  /// \brief The maximum depth to take the execution to.
-  /// Depth is a count of the instructions that have been executed on any
-  /// single path.
   unsigned max_depth;
-
   bool doing_path_exploration;
-
   bool allow_pointer_unsoundness;
-
   bool constant_propagation;
-
   bool self_loops_to_assumptions;
-
   bool simplify_opt;
-
   bool unwinding_assertions;
-
   bool partial_loops;
-
   mp_integer debug_level;
 
   /// \brief Should the additional validation checks be run?
+  ///
   /// If this flag is set the checks for renaming (both level1 and level2) are
   /// executed in the goto_symex_statet (in the assignment method).
   bool run_validation_checks;
@@ -76,37 +68,26 @@ struct symex_configt final
 };
 
 /// \brief The main class for the forward symbolic simulator
-/// \remarks
+///
 /// Higher-level architectural information on symbolic execution is
 /// documented in the \ref symex-overview
 /// "Symbolic execution module page".
 class goto_symext
 {
 public:
-  /// A type abbreviation for \ref goto_symex_statet
   typedef goto_symex_statet statet;
 
-  /// Construct a goto_symext to execute a particular program
-  /// \param mh: The message handler to use for log messages
-  /// \param outer_symbol_table: The symbol table for the program to be
-  ///   executed, excluding any symbols added during the symbolic execution
-  /// \param _target: Where to store the equation built up by this execution
-  /// \param options: The options to use to configure this execution
-  /// \param path_storage: Place to storage symbolic execution paths that have
-  /// been halted and can be resumed later
-  /// \param guard_manager: Manager for creating guards
   goto_symext(
     message_handlert &mh,
     const symbol_tablet &outer_symbol_table,
     symex_target_equationt &_target,
     const optionst &options,
-    path_storaget &path_storage,
-    guard_managert &guard_manager)
+    path_storaget &path_storage)
     : should_pause_symex(false),
       symex_config(options),
+      language_mode(),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
-      guard_manager(guard_manager),
       target(_target),
       atomic_section_counter(0),
       log(mh),
@@ -117,37 +98,21 @@ class goto_symext
   {
   }
 
-  /// A virtual destructor allowing derived classes to be cleaned up correctly
   virtual ~goto_symext() = default;
 
-  /// The type of delegate functions that retrieve a goto_functiont for a
-  /// particular function identifier
-  /// \remarks
-  /// This allows goto_symext to be divorced from the particular type of
-  /// goto_modelt that provides the function bodies
   typedef
     std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
     get_goto_functiont;
 
   /// Return a function to get/load a goto function from the given goto model
-  /// Create a default delegate to retrieve function bodies from a
-  /// goto_functionst
-  /// \param goto_model: The goto model holding the function map from which to
-  ///   retrieve function bodies
-  /// \return A delegate to retrieve function bodies from the given
-  ///   goto_functionst
-  static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model);
-
-  /// \brief Symbolically execute the entire program starting from entry point
-  /// \remarks
-  /// The state that goto_symext maintains uses a lot of memory.
-  /// This method therefore deallocates the state as soon as symbolic execution
-  /// has completed. This function is useful to callers that don't care about
-  /// having the state around afterwards.
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
-  /// \param new_symbol_table: A symbol table to store the symbols added during
-  /// symbolic execution
+  static get_goto_functiont get_goto_function(abstract_goto_modelt &);
+
+  /// \brief symex entire program starting from entry point
+  ///
+  /// The state that goto_symext maintains has a large memory footprint.
+  /// This method deallocates the state as soon as symbolic execution
+  /// has completed, so use it if you don't care about having the state
+  /// around afterwards.
   virtual void symex_from_entry_point_of(
     const get_goto_functiont &get_goto_function,
     symbol_tablet &new_symbol_table);
@@ -158,49 +123,37 @@ class goto_symext
     symbol_tablet &new_symbol_table);
 
   /// Performs symbolic execution using a state and equation that have
-  /// already been used to symbolically execute part of the program. The state
-  /// is not re-initialized; instead, symbolic execution resumes from the
-  /// program counter of the saved state.
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
-  /// \param saved_state: The symbolic execution state to resume from
-  /// \param saved_equation: The equation as previously built up
-  /// \param new_symbol_table: A symbol table to store the symbols added during
-  ///   symbolic execution
+  /// already been used to symex part of the program. The state is not
+  /// re-initialized; instead, symbolic execution resumes from the program
+  /// counter of the saved state.
   virtual void resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
     symex_target_equationt *saved_equation,
     symbol_tablet &new_symbol_table);
 
-  //// \brief Symbolically execute the entire program starting from entry point
+  //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
   /// state, which is useful for examining the state after this method
   /// returns. The state that goto_symext maintains has a large memory
   /// footprint, so if keeping the state around is not necessary,
   /// clients should instead call goto_symext::symex_from_entry_point_of().
-  /// \param state: The symbolic execution state to use for the execution
-  /// \param get_goto_functions: A functor to retrieve function bodies to
-  ///   execute
-  /// \param new_symbol_table: A symbol table to store the symbols added during
-  ///   symbolic execution
   virtual void symex_with_state(
-    statet &state,
-    const get_goto_functiont &get_goto_functions,
-    symbol_tablet &new_symbol_table);
+    statet &,
+    const get_goto_functiont &,
+    symbol_tablet &);
 
-  /// \brief Set when states are pushed onto the workqueue
+  /// \brief Have states been pushed onto the workqueue?
+  ///
   /// If this flag is set at the end of a symbolic execution run, it means that
-  /// symbolic execution has been paused because we encountered a GOTO
-  /// instruction while doing path exploration, and thus pushed the successor
-  /// states of the GOTO onto path_storage. The symbolic execution caller
-  /// should now choose which successor state to continue executing, and resume
-  /// symbolic execution from that state.
+  /// symex has been paused because we encountered a GOTO instruction while
+  /// doing path exploration, and thus pushed the successor states of the GOTO
+  /// onto path_storage. The symbolic execution caller should now choose which
+  /// successor state to continue executing, and resume symex from that state.
   bool should_pause_symex;
 
 protected:
-  /// The configuration to use for this symbolic execution
   const symex_configt symex_config;
 
   /// Initialize the symbolic execution and the given state with
@@ -212,9 +165,8 @@ class goto_symext
 
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.
-  /// \param state: Symbolic execution state for current instruction
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
+  /// \param state: Current GOTO symex step.
+  /// \param get_goto_function: function that retrieves function bodies
   void symex_threaded_step(
     statet &state,
     const get_goto_functiont &get_goto_function);
@@ -260,11 +212,12 @@ class goto_symext
   irep_idt language_mode;
 
 protected:
-  /// The symbol table associated with the goto-program being executed.
-  /// This symbol table will not have objects that are dynamically created as
-  /// part of symbolic execution added to it; those object are stored in the
-  /// symbol table passed as the `new_symbol_table` argument to the `symex_*`
-  /// methods.
+
+  /// The symbol table associated with the goto-program that we're
+  /// executing. This symbol table will not additionally contain objects
+  /// that are dynamically created as part of symbolic execution; the
+  /// names of those object are stored in the symbol table passed as the
+  /// `new_symbol_table` argument to the `symex_*` methods.
   const symbol_tablet &outer_symbol_table;
 
   /// Initialized just before symbolic execution begins, to point to
@@ -275,17 +228,7 @@ class goto_symext
   /// used during symbolic execution to look up names from the original
   /// goto-program, and the names of dynamically-created objects.
   namespacet ns;
-
-  /// Used to create guards. Guards created with different guard managers cannot
-  /// be combined together, so guards created by goto-symex should not escape
-  /// the scope of this manager.
-  guard_managert &guard_manager;
-
-  /// The equation that this execution is building up
   symex_target_equationt &target;
-
-  /// A monotonically increasing index for each encountered ATOMIC_BEGIN
-  /// instruction
   unsigned atomic_section_counter;
 
   /// Variables that should be killed at the end of the current symex_step
@@ -318,9 +261,9 @@ class goto_symext
   /// have any number of ternary expressions mixed with type casts.
   void process_array_expr(statet &, exprt &);
   exprt make_auto_object(const typet &, statet &);
-  virtual void dereference(exprt &, statet &, bool write);
+  virtual void dereference(exprt &, statet &);
 
-  void dereference_rec(exprt &, statet &, bool write);
+  void dereference_rec(exprt &, statet &);
   exprt address_arithmetic(
     const exprt &,
     statet &,
@@ -404,67 +347,38 @@ class goto_symext
     const std::string &msg,
     statet &);
 
-  /// Symbolically execute an ASSUME instruction or simulate such an execution
-  /// for a synthetic assumption
-  /// \param state: Symbolic execution state for current instruction
-  /// \param cond: The guard of the assumption
-  virtual void symex_assume(statet &state, const exprt &cond);
-  void symex_assume_l2(statet &, const exprt &cond);
-
-  /// Merge all branches joining at the current program point. Applies
-  /// \ref merge_goto for each goto state (each of which corresponds to previous
-  /// branch).
-  /// \param state: Symbolic execution state to be updated
-  void merge_gotos(statet &state);
-
-  /// Merge a single branch, the symbolic state of which is held in \p
-  /// goto_state, into the current overall symbolic state. \p goto_state is no
-  /// longer expected to be valid afterwards.
-  /// \param source: source associated with the incoming \p goto_state
-  /// \param goto_state: A state to be merged into this location
-  /// \param state: Symbolic execution state to be updated
-  virtual void merge_goto(
-    const symex_targett::sourcet &source,
-    goto_statet &&goto_state,
-    statet &state);
+  virtual void symex_assume(statet &, const exprt &cond);
+
+  // gotos
+  void merge_gotos(statet &);
 
-  /// Merge the SSA assignments from goto_state into dest_state
-  /// \param goto_state: A state to be merged into this location
-  /// \param dest_state: Symbolic execution state to be updated
-  void phi_function(const goto_statet &goto_state, statet &dest_state);
+  virtual void merge_goto(const goto_statet &goto_state, statet &);
 
-  /// Determine whether to unwind a loop
-  /// \param source
-  /// \param context
-  /// \param unwind
-  /// \return true indicates abort, with false we continue
+  void merge_value_sets(const goto_statet &goto_state, statet &dest);
+
+  void phi_function(const goto_statet &goto_state, statet &);
+
+  // determine whether to unwind a loop -- true indicates abort,
+  // with false we continue.
   virtual bool should_stop_unwind(
     const symex_targett::sourcet &source,
     const call_stackt &context,
     unsigned unwind);
 
-  virtual void loop_bound_exceeded(statet &state, const exprt &guard);
+  virtual void loop_bound_exceeded(statet &, const exprt &guard);
 
-  /// Log a warning that a function has no body
-  /// \param identifier: The name of the function with no body
-  virtual void no_body(const irep_idt &identifier)
+  virtual void no_body(const irep_idt &)
   {
   }
 
-  /// Symbolically execute a FUNCTION_CALL instruction.
+  /// Symbolic execution of a function call.
   /// Only functions that are symbols are supported, see
-  /// \ref goto_symext::symex_function_call_symbol.
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
+  /// \ref goto_symext::symex_function_call_symbol
   virtual void symex_function_call(
-    const get_goto_functiont &get_goto_function,
-    statet &state,
-    const code_function_callt &code);
+    const get_goto_functiont &,
+    statet &,
+    const code_function_callt &);
 
-  /// Symbolically execute a END_FUNCTION instruction.
-  /// \param state: Symbolic execution state for current instruction
   virtual void symex_end_of_function(statet &);
 
   /// Symbolic execution of a call to a function call.
@@ -473,14 +387,10 @@ class goto_symext
   /// \ref goto_symext::symex_fkt
   /// For non-special functions see
   /// \ref goto_symext::symex_function_call_code
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
   virtual void symex_function_call_symbol(
-    const get_goto_functiont &get_goto_function,
-    statet &state,
-    const code_function_callt &code);
+    const get_goto_functiont &,
+    statet &,
+    const code_function_callt &);
 
   /// Symbolic execution of a function call by inlining.
   /// Records the call in \p target by appending a function call step and:
@@ -488,14 +398,10 @@ class goto_symext
   ///    and proceed to executing the code of the function.
   ///   - otherwise assign a nondetministic value to the left-hand-side of the
   ///     call when there is one
-  /// \param get_goto_function: The delegate to retrieve function bodies (see
-  ///   \ref get_goto_functiont)
-  /// \param state: Symbolic execution state for current instruction
-  /// \param call: The function call instruction
   virtual void symex_function_call_code(
-    const get_goto_functiont &get_goto_function,
-    statet &state,
-    const code_function_callt &call);
+    const get_goto_functiont &,
+    statet &,
+    const code_function_callt &);
 
   virtual bool get_unwind_recursion(
     const irep_idt &identifier,
@@ -510,25 +416,17 @@ class goto_symext
   /// \param arguments: arguments that are passed to the function
   void parameter_assignments(
     const irep_idt &function_identifier,
-    const goto_functionst::goto_functiont &goto_function,
-    statet &state,
+    const goto_functionst::goto_functiont &,
+    statet &,
     const exprt::operandst &arguments);
 
   // exceptions
-  /// Symbolically execute a THROW instruction
-  /// \param state: Symbolic execution state for current instruction
-  void symex_throw(statet &state);
-  /// Symbolically execute a CATCH instruction
-  /// \param state: Symbolic execution state for current instruction
-  void symex_catch(statet &state);
+  void symex_throw(statet &);
+  void symex_catch(statet &);
 
-  virtual void do_simplify(exprt &expr);
+  virtual void do_simplify(exprt &);
 
-  /// Symbolically execute an ASSIGN instruction or simulate such an execution
-  /// for a synthetic assignment
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The assignment to execute
-  void symex_assign(statet &state, const code_assignt &code);
+  void symex_assign(statet &, const code_assignt &);
 
   /// Attempt to constant propagate side effects of the assignment (if any)
   ///
@@ -648,7 +546,7 @@ class goto_symext
   // clang-format on
 
   // havocs the given object
-  void havoc_rec(statet &state, const guardt &guard, const exprt &dest);
+  void havoc_rec(statet &, const guardt &, const exprt &);
 
   typedef symex_targett::assignment_typet assignment_typet;
 
@@ -674,57 +572,20 @@ class goto_symext
   /// \param lhs: The expression to assign to
   /// \param code: The `allocate` expression
   virtual void symex_allocate(
-    statet &state,
-    const exprt &lhs,
-    const side_effect_exprt &code);
-  /// Symbolically execute an OTHER instruction that does a CPP `delete`
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The cleaned up CPP `delete` instruction
-  virtual void symex_cpp_delete(statet &state, const codet &code);
-  /// Symbolically execute an assignment instruction that has a CPP `new` or
-  /// `new array` or a Java `new array` on the right hand side
-  /// \param state: Symbolic execution state for current instruction
-  /// \param lhs: The expression to assign to
-  /// \param code: The `new` expression
-  virtual void
-  symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code);
-  /// Symbolically execute a FUNCTION_CALL instruction for a function whose
-  /// name starts with CPROVER_FKT_PREFIX
-  /// \remarks
-  /// While the name seems to imply that this would be called when symbolic
-  /// execution doesn't know what to do, it may actually be derived from a
-  /// German abbreviation for function.
-  /// This should not be called as these functions should already be removed
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
-  virtual void symex_fkt(statet &state, const code_function_callt &code);
-  /// Symbolically execute a FUNCTION_CALL instruction for the `CBMC_trace`
-  /// function
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The function call instruction
-  virtual void symex_trace(statet &state, const code_function_callt &code);
-  /// Symbolically execute an OTHER instruction that does a CPP `printf`
-  /// \param state: Symbolic execution state for current instruction
-  /// \param rhs: The cleaned up CPP `printf` instruction
-  virtual void symex_printf(statet &state, const exprt &rhs);
-  /// Symbolically execute an OTHER instruction that does a CPP input
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The cleaned up input instruction
-  virtual void symex_input(statet &state, const codet &code);
-  /// Symbolically execute an OTHER instruction that does a CPP output
-  /// \param state: Symbolic execution state for current instruction
-  /// \param code: The cleaned up output instruction
-  virtual void symex_output(statet &state, const codet &code);
+    statet &, const exprt &lhs, const side_effect_exprt &);
+  virtual void symex_cpp_delete(statet &, const codet &);
+  virtual void symex_cpp_new(
+    statet &, const exprt &lhs, const side_effect_exprt &);
+  virtual void symex_fkt(statet &, const code_function_callt &);
+  virtual void symex_trace(statet &, const code_function_callt &);
+  virtual void symex_printf(statet &, const irept &);
+  virtual void symex_input(statet &, const codet &);
+  virtual void symex_output(statet &, const codet &);
 
-  /// A monotonically increasing index for each created dynamic object
   static unsigned dynamic_counter;
 
   void rewrite_quantifiers(exprt &, statet &);
 
-  /// \brief Symbolic execution paths to be resumed later
-  /// \remarks
-  /// Partially-executed symbolic execution \ref path_storaget::patht "paths"
-  /// whose execution can be resumed later
   path_storaget &path_storage;
 
 public:
@@ -744,15 +605,14 @@ class goto_symext
   ///
   /// The actual number of total and remaining VCCs should be assigned to
   /// the relevant members of goto_symex_statet. The members below are used to
-  /// cache the values from goto_symex_statet after symbolic execution has
-  /// ended, so that the user of \ref goto_symext can read those values even
-  /// after the state has been deallocated.
+  /// cache the values from goto_symex_statet after symex has ended, so that
+  /// \ref bmct can read those values even after the state has been deallocated.
 
   unsigned _total_vccs, _remaining_vccs;
   ///@}
 
 public:
-  unsigned get_total_vccs() const
+  unsigned get_total_vccs()
   {
     INVARIANT(
       _total_vccs != std::numeric_limits<unsigned>::max(),
@@ -761,7 +621,7 @@ class goto_symext
     return _total_vccs;
   }
 
-  unsigned get_remaining_vccs() const
+  unsigned get_remaining_vccs()
   {
     INVARIANT(
       _remaining_vccs != std::numeric_limits<unsigned>::max(),
@@ -781,7 +641,6 @@ class goto_symext
 /// recursion) being entered. 'Next instruction' in this situation refers
 /// to the next one in program order, so it ignores things like unconditional
 /// GOTOs, and only goes until the end of the current function.
-/// \param state: Symbolic execution state to be transformed
 void symex_transition(goto_symext::statet &state);
 
 void symex_transition(
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 1db7524e09e..f477352d613 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant_utils.h>
 #include <util/optional.h>
 #include <util/pointer_offset_size.h>
-#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
@@ -73,8 +72,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    // to allow constant propagation
-    exprt tmp_size = state.rename(size, ns).get();
+    exprt tmp_size=size;
+    state.rename(tmp_size, ns); // to allow constant propagation
     simplify(tmp_size, ns);
 
     // special treatment for sizeof(T)*x
@@ -141,8 +140,7 @@ void goto_symext::symex_allocate(
 
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
-      size_symbol.name =
-        SYMEX_DYNAMIC_PREFIX + id2string(size_symbol.base_name);
+      size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
       size_symbol.type=tmp_size.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
@@ -161,7 +159,7 @@ void goto_symext::symex_allocate(
   symbolt value_symbol;
 
   value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
-  value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
+  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
   value_symbol.is_lvalue=true;
   value_symbol.type = *object_type;
   value_symbol.type.set(ID_C_dynamic, true);
@@ -374,7 +372,7 @@ void goto_symext::symex_printf(
   statet &state,
   const exprt &rhs)
 {
-  PRECONDITION(!rhs.operands().empty());
+  //PRECONDITION(!rhs.operands().empty());
 
   exprt tmp_rhs = rhs;
   clean_expr(tmp_rhs, state, false);
@@ -422,6 +420,7 @@ void goto_symext::symex_printf(
     target.output_fmt(
       state.guard.as_expr(),
       state.source, "printf", format_string, args);
+#endif
 }
 
 void goto_symext::symex_input(
@@ -430,15 +429,17 @@ void goto_symext::symex_input(
 {
   PRECONDITION(code.operands().size() >= 2);
 
-  exprt id_arg = state.rename(code.op0(), ns).get();
+  exprt id_arg=code.op0();
+
+  state.rename(id_arg, ns);
 
   std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    exprt l2_arg = state.rename(code.operands()[i], ns).get();
-    do_simplify(l2_arg);
-    args.emplace_back(std::move(l2_arg));
+    args.push_back(code.operands()[i]);
+    state.rename(args.back(), ns);
+    do_simplify(args.back());
   }
 
   const irep_idt input_id=get_string_argument(id_arg, ns);
@@ -451,16 +452,18 @@ void goto_symext::symex_output(
   const codet &code)
 {
   PRECONDITION(code.operands().size() >= 2);
-  exprt id_arg = state.rename(code.op0(), ns).get();
 
-  std::list<renamedt<exprt, L2>> args;
+  exprt id_arg=code.op0();
+
+  state.rename(id_arg, ns);
+
+  std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
-    if(symex_config.simplify_opt)
-      l2_arg.simplify(ns);
-    args.emplace_back(l2_arg);
+    args.push_back(code.operands()[i]);
+    state.rename(args.back(), ns);
+    do_simplify(args.back());
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -497,7 +500,7 @@ void goto_symext::symex_cpp_new(
   symbol.base_name=
     do_array?"dynamic_"+count_string+"_array":
              "dynamic_"+count_string+"_value";
-  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
+  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
   symbol.is_lvalue=true;
   if(code.get(ID_statement)==ID_cpp_new_array ||
      code.get(ID_statement)==ID_cpp_new)
@@ -566,12 +569,16 @@ void goto_symext::symex_trace(
 
   if(symex_config.debug_level >= debug_lvl)
   {
-    std::list<renamedt<exprt, L2>> vars;
+    std::list<exprt> vars;
 
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
-      vars.push_back(state.rename(code.arguments()[j], ns));
+    {
+      exprt var(code.arguments()[j]);
+      state.rename(var, ns);
+      vars.push_back(var);
+    }
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }
diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp
index 6115eed0b87..9715e1fb3e0 100644
--- a/src/jsil/jsil_entry_point.cpp
+++ b/src/jsil/jsil_entry_point.cpp
@@ -38,7 +38,7 @@ static void create_initialize(symbol_tablet &symbol_table)
   code_assignt a(rounding_mode, from_integer(0, rounding_mode.type()));
   init_code.add(a);
 
-  initialize.value=init_code;
+  initialize.value = init_code.as_expr();
 
   if(symbol_table.add(initialize))
     throw "failed to add " INITIALIZE_FUNCTION;
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index 5df6bd9c61a..bcb957dc2eb 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -224,7 +224,7 @@ statements: statement
 
 statement: TOK_NEWLINE
          {
-           newstack($$)=code_skipt();
+           newstack($$)=code_skipt().as_expr();
          }
          | instruction TOK_NEWLINE
          {
@@ -255,7 +255,7 @@ instruction: TOK_LABEL TOK_IDENTIFIER
            }
            | TOK_SKIP
            {
-             newstack($$)=code_skipt();
+             newstack($$)=code_skipt().as_expr();
            }
            | TOK_IDENTIFIER TOK_DEFEQ rhs
            {
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index 5408c599c3e..c2067ec5881 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -105,10 +105,8 @@ void static_lifetime_init(
 
   symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
 
-  init_symbol.value=code_blockt();
-  init_symbol.value.add_source_location()=source_location;
-
-  code_blockt &dest=to_code_block(to_code(init_symbol.value));
+  code_blockt dest;
+  dest.add_source_location() = source_location;
 
   // add the magic label to hide
   dest.add(code_labelt(CPROVER_PREFIX "HIDE", code_skipt()));
@@ -160,4 +158,6 @@ void static_lifetime_init(
       dest.add(function_call);
     }
   }
+
+  init_symbol.value = dest.as_expr();
 }
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index c4b71a0015b..6e2059a5871 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -309,49 +309,59 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
               << format(if_expr.true_case()) << " : "
               << format(if_expr.false_case()) << ')';
   }
-  else if(id == ID_code)
-  {
-    const auto &code = to_code(expr);
-    const irep_idt &statement = code.get_statement();
+  else
+    return fallback_format_rec(os, expr);
+}
 
-    if(statement == ID_assign)
-      return os << format(to_code_assign(code).lhs()) << " = "
-                << format(to_code_assign(code).rhs()) << ';';
-    else if(statement == ID_block)
-    {
-      os << '{';
-      for(const auto &s : to_code_block(code).statements())
-        os << ' ' << format(s);
-      return os << " }";
-    }
-    else if(statement == ID_dead)
-    {
-      return os << "dead " << format(to_code_dead(code).symbol()) << ";";
-    }
-    else if(statement == ID_decl)
-    {
-      const auto &declaration_symb = to_code_decl(code).symbol();
-      return os << "decl " << format(declaration_symb.type()) << " "
-                << format(declaration_symb) << ";";
-    }
-    else if(statement == ID_function_call)
-    {
-      const auto &func_call = to_code_function_call(code);
-      os << to_symbol_expr(func_call.function()).get_identifier() << "(";
-
-      // Join all our arguments together.
-      join_strings(
-        os,
-        func_call.arguments().begin(),
-        func_call.arguments().end(),
-        ", ",
-        [](const exprt &expr) { return format(expr); });
-
-      return os << ");";
-    }
-    else
-      return fallback_format_rec(os, expr);
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(std::ostream &os, const codet &code)
+{
+  const irep_idt &statement = code.get_statement();
+
+  if(statement == ID_assign)
+    return os << format(to_code_assign(code).lhs()) << " = "
+              << format(to_code_assign(code).rhs()) << ';';
+  else if(statement == ID_block)
+  {
+    os << '{';
+    for(const auto &s : to_code_block(code).statements())
+      os << ' ' << format(s);
+    return os << " }";
+  }
+  else if(statement == ID_dead)
+  {
+    return os << "dead " << format(to_code_dead(code).symbol()) << ";";
+  }
+  else if(statement == ID_decl)
+  {
+    const auto &declaration_symb = to_code_decl(code).symbol();
+    return os << "decl " << format(declaration_symb.type()) << " "
+              << format(declaration_symb) << ";";
+  }
+  else if(statement == ID_function_call)
+  {
+    const auto &func_call = to_code_function_call(code);
+    os << to_symbol_expr(func_call.function()).get_identifier() << "(";
+
+    // Join all our arguments together.
+    join_strings(
+      os,
+      func_call.arguments().begin(),
+      func_call.arguments().end(),
+      ", ",
+      [](const exprt &expr) { return format(expr); });
+
+    return os << ");";
+  }
+  else if(statement == ID_block)
+  {
+    os << '{';
+    for(const auto &s : to_code_block(code).statements())
+      os << ' ' << format(s);
+    return os << " }";
   }
   else
-    return fallback_format_rec(os, expr);
+    return os << statement;
 }
diff --git a/src/util/format_expr.h b/src/util/format_expr.h
index eed9d013973..074b108e313 100644
--- a/src/util/format_expr.h
+++ b/src/util/format_expr.h
@@ -12,8 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr.h"
 #include "format.h"
 
+class codet;
+
 //! Formats an expression in a generic syntax
 //! that is inspired by C/C++/Java, and is meant for debugging
 std::ostream &format_rec(std::ostream &, const exprt &);
+std::ostream &format_rec(std::ostream &, const codet &);
 
 #endif // CPROVER_UTIL_FORMAT_EXPR_H
diff --git a/src/util/std_code.h b/src/util/std_code.h
index aba10d679eb..333da0ac8de 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -31,36 +31,41 @@ Author: Daniel Kroening, kroening@kroening.com
 /// To distinguish a `codet` from other [exprts](\ref exprt), we set its
 /// [id()](\ref irept::id) to `ID_code`. To distinguish different types of
 /// `codet`, we use a named sub `ID_statement`.
-class codet:public exprt
+class codet : public irept
 {
 public:
+  DEPRECATED("Use codet(statement) instead")
+  codet() : irept(ID_code)
+  {
+  }
+
   /// \param statement: Specifies the type of the `codet` to be constructed,
   ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
   ///   \ref code_assignt.
-  explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet())
+  explicit codet(const irep_idt &statement) : irept(ID_code)
   {
     set_statement(statement);
   }
 
-  codet(const irep_idt &statement, source_locationt loc)
-    : exprt(ID_code, empty_typet(), std::move(loc))
+  codet(const irep_idt &statement, source_locationt loc) : irept(ID_code)
   {
     set_statement(statement);
+    add_source_location() = std::move(loc);
   }
 
   /// \param statement: Specifies the type of the `codet` to be constructed,
   ///   e.g. `ID_block` for a \ref code_blockt or `ID_assign` for a
   ///   \ref code_assignt.
   /// \param _op: any operands to be added
-  explicit codet(const irep_idt &statement, operandst _op) : codet(statement)
+  explicit codet(const irep_idt &statement, irept::subt _sub) : codet(statement)
   {
-    operands() = std::move(_op);
+    get_sub() = std::move(_sub);
   }
 
-  codet(const irep_idt &statement, operandst op, source_locationt loc)
+  codet(const irep_idt &statement, irept::subt _sub, source_locationt loc)
     : codet(statement, std::move(loc))
   {
-    operands() = std::move(op);
+    get_sub() = std::move(_sub);
   }
 
   void set_statement(const irep_idt &statement)
@@ -126,45 +131,174 @@ class codet:public exprt
     check_code(code, vm);
   }
 
-  using exprt::op0;
-  using exprt::op1;
-  using exprt::op2;
-  using exprt::op3;
+  const source_locationt &find_source_location() const;
+
+  const source_locationt &source_location() const
+  {
+    return static_cast<const source_locationt &>(find(ID_C_source_location));
+  }
+
+  source_locationt &add_source_location()
+  {
+    return static_cast<source_locationt &>(add(ID_C_source_location));
+  }
+
+  const exprt &as_expr() const
+  {
+    return *static_cast<const exprt *>(static_cast<const irept *>(this));
+  }
+
+public:
+  // will rename to expr_operandst
+  typedef std::vector<exprt> operandst;
+
+  // returns true if there is at least one operand
+  bool has_operands() const
+  {
+    return !operands().empty();
+  }
+
+  operandst &operands()
+  {
+    return (operandst &)get_sub();
+  }
+
+  const operandst &operands() const
+  {
+    return (const operandst &)get_sub();
+  }
+
+  exprt &op0()
+  {
+    return operands().front();
+  }
+
+  exprt &op1()
+  {
+    return operands()[1];
+  }
+
+  exprt &op2()
+  {
+    return operands()[2];
+  }
+
+  exprt &op3()
+  {
+    return operands()[3];
+  }
+
+  const exprt &op0() const
+  {
+    return operands().front();
+  }
+
+  const exprt &op1() const
+  {
+    return operands()[1];
+  }
+
+  const exprt &op2() const
+  {
+    return operands()[2];
+  }
+
+  const exprt &op3() const
+  {
+    return operands()[3];
+  }
+
+  void reserve_operands(operandst::size_type n)
+  {
+    operands().reserve(n);
+  }
+
+  // destroys expr, e1, e2, e3
+  void move_to_operands(exprt &);
+  void move_to_operands(exprt &, exprt &);
+  void move_to_operands(exprt &, exprt &, exprt &);
+  // does not destroy expr, e1, e2, e3
+  void copy_to_operands(const exprt &);
+  void copy_to_operands(const exprt &, const exprt &);
+  void copy_to_operands(const exprt &, const exprt &, const exprt &);
+  void add_to_operands(const exprt &);
+  void add_to_operands(const exprt &, const exprt &);
+  void add_to_operands(const exprt &, const exprt &, const exprt &);
+
+protected:
+  typedef std::vector<codet> code_operandst;
+
+  code_operandst &code_operands()
+  { return (code_operandst &)get_sub(); }
+
+  const code_operandst &code_operands() const
+  { return (const code_operandst &)get_sub(); }
+
+  codet &code_op0()
+  { return code_operands().front(); }
+
+  codet &code_op1()
+  { return code_operands()[1]; }
+
+  codet &code_op2()
+  { return code_operands()[2]; }
+
+  codet &code_op3()
+  { return code_operands()[3]; }
+
+  const codet &code_op0() const
+  { return code_operands().front(); }
+
+  const codet &code_op1() const
+  { return code_operands()[1]; }
+
+  const codet &code_op2() const
+  { return code_operands()[2]; }
+
+  const codet &code_op3() const
+  { return code_operands()[3]; }
+
+  // destroys expr, e1, e2, e3
+  void move_to_operands(codet &);
+  void move_to_operands(codet &, codet &);
+  void move_to_operands(codet &, codet &, codet &);
+  // does not destroy expr, e1, e2, e3
+  void copy_to_operands(const codet &);
+  void copy_to_operands(const codet &, const codet &);
+  void copy_to_operands(const codet &, const codet &, const codet &);
+
+public:
+  void add_to_operands(const codet &);
+  void add_to_operands(const codet &, const codet &);
+  void add_to_operands(const codet &, const codet &, const codet &);
 };
 
 namespace detail // NOLINT
 {
-
-template<typename Tag>
-inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
+template <typename Tag>
+inline bool can_cast_code_impl(const codet &code, const Tag &tag)
 {
-  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
-  {
-    return ptr->get_statement() == tag;
-  }
-  return false;
+  return code.get_statement() == tag;
 }
 
 } // namespace detail
 
-template<> inline bool can_cast_expr<codet>(const exprt &base)
-{
-  return base.id()==ID_code;
-}
+template <typename T>
+inline bool can_cast_code(const codet &base);
 
 // to_code has no validation other than checking the id(), so no validate_expr
 // is provided for codet
 
-inline const codet &to_code(const exprt &expr)
+inline const codet &to_code(const irept &irep)
 {
-  PRECONDITION(expr.id() == ID_code);
-  return static_cast<const codet &>(expr);
+  PRECONDITION(irep.id() == ID_code);
+  return static_cast<const codet &>(irep);
 }
 
-inline codet &to_code(exprt &expr)
+inline codet &to_code(irept &irep)
 {
-  PRECONDITION(expr.id() == ID_code);
-  return static_cast<codet &>(expr);
+  PRECONDITION(irep.id() == ID_code);
+  return static_cast<codet &>(irep);
 }
 
 /// A \ref codet representing sequential composition of program statements.
@@ -191,20 +325,20 @@ class code_blockt:public codet
   static code_blockt from_list(const std::list<codet> &_list)
   {
     code_blockt result;
-    auto &s=result.statements();
-    s.reserve(_list.size());
-    for(const auto &c : _list)
-      s.push_back(c);
+    auto &o = result.statements();
+    o.reserve(_list.size());
+    for(const auto &statement : _list)
+      o.push_back(statement);
     return result;
   }
 
   explicit code_blockt(const std::vector<codet> &_statements)
-    : codet(ID_block, (const std::vector<exprt> &)_statements)
+    : codet(ID_block, (const irept::subt &)_statements)
   {
   }
 
   explicit code_blockt(std::vector<codet> &&_statements)
-    : codet(ID_block, std::move((std::vector<exprt> &&) _statements))
+    : codet(ID_block, std::move((irept::subt &&) _statements))
   {
   }
 
@@ -248,7 +382,8 @@ class code_blockt:public codet
   }
 };
 
-template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_blockt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_block);
 }
@@ -283,7 +418,8 @@ class code_skipt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_skipt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_skip);
 }
@@ -373,7 +509,20 @@ class code_assignt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
+inline void validate_operands(
+  const codet &value,
+  exprt::operandst::size_type number,
+  const char *message,
+  bool allow_more = false)
+{
+  DATA_INVARIANT(
+    allow_more ? value.operands().size() >= number
+               : value.operands().size() == number,
+    message);
+}
+
+template <>
+inline bool can_cast_code<code_assignt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_assign);
 }
@@ -440,7 +589,8 @@ class code_declt:public codet
   }
 };
 
-template<> inline bool can_cast_expr<code_declt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_declt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_decl);
 }
@@ -509,7 +659,8 @@ class code_deadt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_deadt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_dead);
 }
@@ -558,7 +709,8 @@ class code_assumet:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
+template <>
+inline bool can_cast_code<code_assumet>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_assume);
 }
@@ -610,7 +762,8 @@ class code_assertt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_assertt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_assert);
 }
@@ -672,11 +825,13 @@ class code_inputt : public codet
     const validation_modet vm = validation_modet::INVARIANT);
 };
 
+#if 0
 template <>
-inline bool can_cast_expr<code_inputt>(const exprt &base)
+inline bool can_cast_expr<code_inputt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_input);
 }
+#endif
 
 inline void validate_expr(const code_inputt &input)
 {
@@ -718,11 +873,13 @@ class code_outputt : public codet
     const validation_modet vm = validation_modet::INVARIANT);
 };
 
+#if 0
 template <>
 inline bool can_cast_expr<code_outputt>(const exprt &base)
 {
   return detail::can_cast_code_impl(base, ID_output);
 }
+#endif
 
 inline void validate_expr(const code_outputt &output)
 {
@@ -788,7 +945,7 @@ class code_ifthenelset:public codet
 
   const codet &then_case() const
   {
-    return static_cast<const codet &>(op1());
+    return code_op1();
   }
 
   bool has_else_case() const
@@ -798,17 +955,17 @@ class code_ifthenelset:public codet
 
   const codet &else_case() const
   {
-    return static_cast<const codet &>(op2());
+    return code_op2();
   }
 
   codet &then_case()
   {
-    return static_cast<codet &>(op1());
+    return code_op1();
   }
 
   codet &else_case()
   {
-    return static_cast<codet &>(op2());
+    return code_op2();
   }
 
 protected:
@@ -818,7 +975,8 @@ class code_ifthenelset:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
+template <>
+inline bool can_cast_code<code_ifthenelset>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_ifthenelse);
 }
@@ -865,12 +1023,12 @@ class code_switcht:public codet
 
   const codet &body() const
   {
-    return to_code(op1());
+    return code_op1();
   }
 
   codet &body()
   {
-    return static_cast<codet &>(op1());
+    return code_op1();
   }
 
 protected:
@@ -880,7 +1038,8 @@ class code_switcht:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
+template <>
+inline bool can_cast_code<code_switcht>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_switch);
 }
@@ -927,12 +1086,12 @@ class code_whilet:public codet
 
   const codet &body() const
   {
-    return to_code(op1());
+    return code_op1();
   }
 
   codet &body()
   {
-    return static_cast<codet &>(op1());
+    return code_op1();
   }
 
 protected:
@@ -942,7 +1101,8 @@ class code_whilet:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
+template <>
+inline bool can_cast_code<code_whilet>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_while);
 }
@@ -989,12 +1149,12 @@ class code_dowhilet:public codet
 
   const codet &body() const
   {
-    return to_code(op1());
+    return code_op1();
   }
 
   codet &body()
   {
-    return static_cast<codet &>(op1());
+    return code_op1();
   }
 
 protected:
@@ -1004,7 +1164,8 @@ class code_dowhilet:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
+template <>
+inline bool can_cast_code<code_dowhilet>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_dowhile);
 }
@@ -1086,12 +1247,12 @@ class code_fort:public codet
 
   const codet &body() const
   {
-    return to_code(op3());
+    return code_op3();
   }
 
   codet &body()
   {
-    return static_cast<codet &>(op3());
+    return code_op3();
   }
 
 protected:
@@ -1101,7 +1262,8 @@ class code_fort:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_fort>(const exprt &base)
+template <>
+inline bool can_cast_code<code_fort>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_for);
 }
@@ -1153,7 +1315,8 @@ class code_gotot:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
+template <>
+inline bool can_cast_code<code_gotot>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_goto);
 }
@@ -1286,7 +1449,8 @@ class code_function_callt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_function_callt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_function_call);
 }
@@ -1351,7 +1515,8 @@ class code_returnt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_returnt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_return);
 }
@@ -1404,12 +1569,12 @@ class code_labelt:public codet
 
   codet &code()
   {
-    return static_cast<codet &>(op0());
+    return code_op0();
   }
 
   const codet &code() const
   {
-    return static_cast<const codet &>(op0());
+    return code_op0();
   }
 
 protected:
@@ -1419,7 +1584,8 @@ class code_labelt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_labelt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_label);
 }
@@ -1477,12 +1643,12 @@ class code_switch_caset:public codet
 
   codet &code()
   {
-    return static_cast<codet &>(op1());
+    return code_op1();
   }
 
   const codet &code() const
   {
-    return static_cast<const codet &>(op1());
+    return code_op1();
   }
 
 protected:
@@ -1492,7 +1658,8 @@ class code_switch_caset:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
+template <>
+inline bool can_cast_code<code_switch_caset>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_switch_case);
 }
@@ -1558,13 +1725,13 @@ class code_gcc_switch_case_ranget : public codet
   /// the statement to be executed when the case applies
   codet &code()
   {
-    return static_cast<codet &>(op2());
+    return static_cast<codet &>(get_sub()[2]);
   }
 
   /// the statement to be executed when the case applies
   const codet &code() const
   {
-    return static_cast<const codet &>(op2());
+    return static_cast<const codet &>(get_sub()[2]);
   }
 
 protected:
@@ -1574,24 +1741,13 @@ class code_gcc_switch_case_ranget : public codet
   using codet::op3;
 };
 
-template <>
-inline bool can_cast_expr<code_gcc_switch_case_ranget>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_gcc_switch_case_range);
-}
-
-inline void validate_expr(const code_gcc_switch_case_ranget &x)
-{
-  validate_operands(x, 3, "gcc-switch-case-range must have three operands");
-}
-
 inline const code_gcc_switch_case_ranget &
 to_code_gcc_switch_case_range(const codet &code)
 {
   PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
   const code_gcc_switch_case_ranget &ret =
     static_cast<const code_gcc_switch_case_ranget &>(code);
-  validate_expr(ret);
+  //validate_expr(ret);
   return ret;
 }
 
@@ -1600,7 +1756,7 @@ inline code_gcc_switch_case_ranget &to_code_gcc_switch_case_range(codet &code)
   PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
   code_gcc_switch_case_ranget &ret =
     static_cast<code_gcc_switch_case_ranget &>(code);
-  validate_expr(ret);
+  //validate_expr(ret);
   return ret;
 }
 
@@ -1620,7 +1776,8 @@ class code_breakt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_breakt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_break);
 }
@@ -1656,7 +1813,8 @@ class code_continuet:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
+template <>
+inline bool can_cast_code<code_continuet>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_continue);
 }
@@ -1699,7 +1857,8 @@ class code_asmt:public codet
   }
 };
 
-template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_asmt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_asm);
 }
@@ -1787,12 +1946,6 @@ class code_asm_gcct : public code_asmt
   using code_asmt::op3;
 };
 
-template <>
-inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
-{
-  return detail::can_cast_code_impl(base, ID_asm);
-}
-
 inline void validate_expr(const code_asm_gcct &x)
 {
   validate_operands(x, 5, "code_asm_gcc must have five operands");
@@ -1843,7 +1996,8 @@ class code_expressiont:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
+template <>
+inline bool can_cast_code<code_expressiont>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_expression);
 }
@@ -2089,20 +2243,21 @@ class side_effect_expr_statement_expressiont : public side_effect_exprt
     source_locationt loc)
     : side_effect_exprt(
         ID_statement_expression,
-        {std::move(_code)},
+        {},
         std::move(_type),
         std::move(loc))
   {
+    set(ID_statement, std::move(_code));
   }
 
   codet &statement()
   {
-    return to_code(op0());
+    return static_cast<codet &>(add(ID_statement));
   }
 
   const codet &statement() const
   {
-    return to_code(op0());
+    return static_cast<const codet &>(find(ID_statement));
   }
 };
 
@@ -2338,7 +2493,8 @@ class code_push_catcht:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
+template <>
+inline bool can_cast_code<code_push_catcht>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_push_catch);
 }
@@ -2375,7 +2531,8 @@ class code_pop_catcht:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
+template <>
+inline bool can_cast_code<code_pop_catcht>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_pop_catch);
 }
@@ -2400,7 +2557,7 @@ static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
 /// landingpadt(symbol_expr("e", ...)))
 class code_landingpadt:public codet
 {
- public:
+public:
   code_landingpadt():codet(ID_exception_landingpad)
   {
     operands().resize(1);
@@ -2415,6 +2572,7 @@ class code_landingpadt:public codet
   {
     return op0();
   }
+
   exprt &catch_expr()
   {
     return op0();
@@ -2427,7 +2585,8 @@ class code_landingpadt:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
+template <>
+inline bool can_cast_code<code_landingpadt>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_exception_landingpad);
 }
@@ -2465,12 +2624,12 @@ class code_try_catcht:public codet
 
   codet &try_code()
   {
-    return static_cast<codet &>(op0());
+    return code_op0();
   }
 
   const codet &try_code() const
   {
-    return static_cast<const codet &>(op0());
+    return code_op0();
   }
 
   code_declt &get_catch_decl(unsigned i)
@@ -2509,7 +2668,8 @@ class code_try_catcht:public codet
   using codet::op3;
 };
 
-template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
+template <>
+inline bool can_cast_code<code_try_catcht>(const codet &base)
 {
   return detail::can_cast_code_impl(base, ID_try_catch);
 }
diff --git a/src/util/typecheck.h b/src/util/typecheck.h
index aed223a0b90..a1b3193a6d0 100644
--- a/src/util/typecheck.h
+++ b/src/util/typecheck.h
@@ -10,8 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_TYPECHECK_H
 #define CPROVER_UTIL_TYPECHECK_H
 
-#include "expr.h"
 #include "message.h"
+#include "std_code.h"
 
 class typecheckt:public messaget
 {