diff --git a/src/goto-programs/goto_instruction_code.h b/src/goto-programs/goto_instruction_code.h
index 9d9b509e611..3b105396e57 100644
--- a/src/goto-programs/goto_instruction_code.h
+++ b/src/goto-programs/goto_instruction_code.h
@@ -13,25 +13,30 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/std_code_base.h>
 #include <util/std_expr.h>
 
-/// A \ref codet representing an assignment in the program.
+using goto_instruction_codet = codet;
+
+/// A \ref goto_instruction_codet representing an assignment in the program.
 /// For example, if an expression `e1` is represented as an \ref exprt `expr1`
 /// and an expression `e2` is represented as an \ref exprt `expr2`, the
 /// assignment `e1 = e2;` can be represented as `code_assignt(expr1, expr2)`.
-class code_assignt : public codet
+class code_assignt : public goto_instruction_codet
 {
 public:
-  code_assignt() : codet(ID_assign)
+  code_assignt() : goto_instruction_codet(ID_assign)
   {
     operands().resize(2);
   }
 
   code_assignt(exprt lhs, exprt rhs)
-    : codet(ID_assign, {std::move(lhs), std::move(rhs)})
+    : goto_instruction_codet(ID_assign, {std::move(lhs), std::move(rhs)})
   {
   }
 
   code_assignt(exprt lhs, exprt rhs, source_locationt loc)
-    : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc))
+    : goto_instruction_codet(
+        ID_assign,
+        {std::move(lhs), std::move(rhs)},
+        std::move(loc))
   {
   }
 
@@ -56,7 +61,7 @@ class code_assignt : public codet
   }
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
@@ -64,7 +69,7 @@ class code_assignt : public codet
   }
 
   static void validate(
-    const codet &code,
+    const goto_instruction_codet &code,
     const namespacet &,
     const validation_modet vm = validation_modet::INVARIANT)
   {
@@ -77,7 +82,7 @@ class code_assignt : public codet
   }
 
   static void validate_full(
-    const codet &code,
+    const goto_instruction_codet &code,
     const namespacet &ns,
     const validation_modet vm = validation_modet::INVARIANT)
   {
@@ -90,10 +95,10 @@ class code_assignt : public codet
   }
 
 protected:
-  using codet::op0;
-  using codet::op1;
-  using codet::op2;
-  using codet::op3;
+  using goto_instruction_codet::op0;
+  using goto_instruction_codet::op1;
+  using goto_instruction_codet::op2;
+  using goto_instruction_codet::op3;
 };
 
 template <>
@@ -107,26 +112,27 @@ inline void validate_expr(const code_assignt &x)
   code_assignt::check(x);
 }
 
-inline const code_assignt &to_code_assign(const codet &code)
+inline const code_assignt &to_code_assign(const goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_assign);
   code_assignt::check(code);
   return static_cast<const code_assignt &>(code);
 }
 
-inline code_assignt &to_code_assign(codet &code)
+inline code_assignt &to_code_assign(goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_assign);
   code_assignt::check(code);
   return static_cast<code_assignt &>(code);
 }
 
-/// A \ref codet representing the removal of a local variable going out of
-/// scope.
-class code_deadt : public codet
+/// A \ref goto_instruction_codet representing the removal of
+/// a local variable going out of scope.
+class code_deadt : public goto_instruction_codet
 {
 public:
-  explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)})
+  explicit code_deadt(symbol_exprt symbol)
+    : goto_instruction_codet(ID_dead, {std::move(symbol)})
   {
   }
 
@@ -146,7 +152,7 @@ class code_deadt : public codet
   }
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
@@ -160,10 +166,10 @@ class code_deadt : public codet
   }
 
 protected:
-  using codet::op0;
-  using codet::op1;
-  using codet::op2;
-  using codet::op3;
+  using goto_instruction_codet::op0;
+  using goto_instruction_codet::op1;
+  using goto_instruction_codet::op2;
+  using goto_instruction_codet::op3;
 };
 
 template <>
@@ -177,28 +183,29 @@ inline void validate_expr(const code_deadt &x)
   code_deadt::check(x);
 }
 
-inline const code_deadt &to_code_dead(const codet &code)
+inline const code_deadt &to_code_dead(const goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_dead);
   code_deadt::check(code);
   return static_cast<const code_deadt &>(code);
 }
 
-inline code_deadt &to_code_dead(codet &code)
+inline code_deadt &to_code_dead(goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_dead);
   code_deadt::check(code);
   return static_cast<code_deadt &>(code);
 }
 
-/// A `codet` representing the declaration of a local variable.
+/// A `goto_instruction_codet` representing the declaration of a local variable.
 /// For example, if a variable (symbol) `x` is represented as a
 /// \ref symbol_exprt `sym`, then the declaration of this variable can be
 /// represented as `code_declt(sym)`.
-class code_declt : public codet
+class code_declt : public goto_instruction_codet
 {
 public:
-  explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
+  explicit code_declt(symbol_exprt symbol)
+    : goto_instruction_codet(ID_decl, {std::move(symbol)})
   {
   }
 
@@ -218,7 +225,7 @@ class code_declt : public codet
   }
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
@@ -242,30 +249,30 @@ inline void validate_expr(const code_declt &x)
   code_declt::check(x);
 }
 
-inline const code_declt &to_code_decl(const codet &code)
+inline const code_declt &to_code_decl(const goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_decl);
   code_declt::check(code);
   return static_cast<const code_declt &>(code);
 }
 
-inline code_declt &to_code_decl(codet &code)
+inline code_declt &to_code_decl(goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_decl);
   code_declt::check(code);
   return static_cast<code_declt &>(code);
 }
 
-/// \ref codet representation of a function call statement.
+/// \ref goto_instruction_codet representation of a function call statement.
 /// The function call statement has three operands.
 /// The first is the expression that is used to store the return value.
 /// The second is the function called.
 /// The third is a vector of argument values.
-class code_function_callt : public codet
+class code_function_callt : public goto_instruction_codet
 {
 public:
   explicit code_function_callt(exprt _function)
-    : codet(
+    : goto_instruction_codet(
         ID_function_call,
         {nil_exprt(), std::move(_function), exprt(ID_arguments)})
   {
@@ -274,7 +281,7 @@ class code_function_callt : public codet
   typedef exprt::operandst argumentst;
 
   code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
-    : codet(
+    : goto_instruction_codet(
         ID_function_call,
         {std::move(_lhs), std::move(_function), exprt(ID_arguments)})
   {
@@ -318,7 +325,7 @@ class code_function_callt : public codet
   }
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
@@ -330,7 +337,7 @@ class code_function_callt : public codet
   }
 
   static void validate(
-    const codet &code,
+    const goto_instruction_codet &code,
     const namespacet &,
     const validation_modet vm = validation_modet::INVARIANT)
   {
@@ -344,7 +351,7 @@ class code_function_callt : public codet
   }
 
   static void validate_full(
-    const codet &code,
+    const goto_instruction_codet &code,
     const namespacet &ns,
     const validation_modet vm = validation_modet::INVARIANT)
   {
@@ -357,10 +364,10 @@ class code_function_callt : public codet
   }
 
 protected:
-  using codet::op0;
-  using codet::op1;
-  using codet::op2;
-  using codet::op3;
+  using goto_instruction_codet::op0;
+  using goto_instruction_codet::op1;
+  using goto_instruction_codet::op2;
+  using goto_instruction_codet::op3;
 };
 
 template <>
@@ -374,29 +381,30 @@ inline void validate_expr(const code_function_callt &x)
   code_function_callt::check(x);
 }
 
-inline const code_function_callt &to_code_function_call(const codet &code)
+inline const code_function_callt &
+to_code_function_call(const goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_function_call);
   code_function_callt::check(code);
   return static_cast<const code_function_callt &>(code);
 }
 
-inline code_function_callt &to_code_function_call(codet &code)
+inline code_function_callt &to_code_function_call(goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_function_call);
   code_function_callt::check(code);
   return static_cast<code_function_callt &>(code);
 }
 
-/// A `codet` representing the declaration that an input of a particular
-/// description has a value which corresponds to the value of a given expression
-/// (or expressions).
+/// A `goto_instruction_codet` representing the declaration that an input of
+/// a particular description has a value which corresponds to the value of a
+/// given expression (or expressions).
 /// When working with the C front end, calls to the `__CPROVER_input` intrinsic
 /// can be added to the input code in order add instructions of this type to the
 /// goto program.
 /// The first argument is expected to be a C string denoting the input
 /// identifier. The second argument is the expression for the input value.
-class code_inputt : public codet
+class code_inputt : public goto_instruction_codet
 {
 public:
   /// This constructor is for support of calls to `__CPROVER_input` in user
@@ -420,7 +428,7 @@ class code_inputt : public codet
     optionalt<source_locationt> location = {});
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT);
 };
 
@@ -435,15 +443,15 @@ inline void validate_expr(const code_inputt &input)
   code_inputt::check(input);
 }
 
-/// A `codet` representing the declaration that an output of a particular
-/// description has a value which corresponds to the value of a given expression
-/// (or expressions).
+/// A `goto_instruction_codet` representing the declaration that an output of
+/// a particular description has a value which corresponds to the value of a
+/// given expression (or expressions).
 /// When working with the C front end, calls to the `__CPROVER_output` intrinsic
 /// can be added to the input code in order add instructions of this type to the
 /// goto program.
 /// The first argument is expected to be a C string denoting the output
 /// identifier. The second argument is the expression for the output value.
-class code_outputt : public codet
+class code_outputt : public goto_instruction_codet
 {
 public:
   /// This constructor is for support of calls to `__CPROVER_output` in user
@@ -466,7 +474,7 @@ class code_outputt : public codet
     optionalt<source_locationt> location = {});
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT);
 };
 
@@ -481,11 +489,13 @@ inline void validate_expr(const code_outputt &output)
   code_outputt::check(output);
 }
 
-/// \ref codet representation of a "return from a function" statement.
-class code_returnt : public codet
+/// \ref goto_instruction_codet representation of a "return from a
+/// function" statement.
+class code_returnt : public goto_instruction_codet
 {
 public:
-  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
+  explicit code_returnt(exprt _op)
+    : goto_instruction_codet(ID_return, {std::move(_op)})
   {
   }
 
@@ -500,17 +510,17 @@ class code_returnt : public codet
   }
 
   static void check(
-    const codet &code,
+    const goto_instruction_codet &code,
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
   }
 
 protected:
-  using codet::op0;
-  using codet::op1;
-  using codet::op2;
-  using codet::op3;
+  using goto_instruction_codet::op0;
+  using goto_instruction_codet::op1;
+  using goto_instruction_codet::op2;
+  using goto_instruction_codet::op3;
 };
 
 template <>
@@ -524,14 +534,14 @@ inline void validate_expr(const code_returnt &x)
   code_returnt::check(x);
 }
 
-inline const code_returnt &to_code_return(const codet &code)
+inline const code_returnt &to_code_return(const goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
   code_returnt::check(code);
   return static_cast<const code_returnt &>(code);
 }
 
-inline code_returnt &to_code_return(codet &code)
+inline code_returnt &to_code_return(goto_instruction_codet &code)
 {
   PRECONDITION(code.get_statement() == ID_return);
   code_returnt::check(code);
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index 87be6590b5a..9e3199079b6 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -99,7 +99,7 @@ class goto_programt
   /// - type:  an enum value describing the action performed by this instruction
   /// - guard: an (arbitrarily complex) expression (usually an \ref exprt) of
   ///          Boolean type
-  /// - code:  a code statement (usually a \ref codet)
+  /// - code:  a code statement (usually a \ref goto_instruction_codet)
   ///
   /// The meaning of an instruction node depends on the `type` field. Different
   /// kinds of instructions make use of the fields `guard` and `code` for
@@ -131,8 +131,9 @@ class goto_programt
   ///     Update the left-hand side of `code` (an instance of code_assignt) to
   ///     the value of the right-hand side.
   /// - OTHER:
-  ///     Execute the `code` (an instance of codet of kind ID_fence, ID_printf,
-  ///     ID_array_copy, ID_array_set, ID_input, ID_output, ...).
+  ///     Execute the `code` (an instance of goto_instruction_codet of kind
+  ///     ID_fence, ID_printf, ID_array_copy, ID_array_set, ID_input,
+  ///     ID_output, ...).
   /// - ASSUME:
   ///     This thread of execution waits for `guard` to evaluate to true.
   ///     Assume does not "retro-actively" affect the thread or any ASSERTs.
@@ -180,17 +181,17 @@ class goto_programt
   {
   protected:
     /// Do not read or modify directly -- use get_X() instead
-    codet code;
+    goto_instruction_codet code;
 
   public:
     /// Get the code represented by this instruction
-    const codet &get_code() const
+    const goto_instruction_codet &get_code() const
     {
       return code;
     }
 
     /// Set the code represented by this instruction
-    codet &code_nonconst()
+    goto_instruction_codet &code_nonconst()
     {
       return code;
     }
@@ -310,14 +311,14 @@ class goto_programt
     }
 
     /// Get the statement for OTHER
-    const codet &get_other() const
+    const goto_instruction_codet &get_other() const
     {
       PRECONDITION(is_other());
       return code;
     }
 
     /// Set the statement for OTHER
-    void set_other(codet &c)
+    void set_other(goto_instruction_codet &c)
     {
       PRECONDITION(is_other());
       code = std::move(c);
@@ -496,7 +497,7 @@ class goto_programt
     }
 
     explicit instructiont(goto_program_instruction_typet __type)
-      : code(static_cast<const codet &>(get_nil_irep())),
+      : code(static_cast<const goto_instruction_codet &>(get_nil_irep())),
         _source_location(source_locationt::nil()),
         _type(__type),
         guard(true_exprt())
@@ -505,7 +506,7 @@ class goto_programt
 
     /// Constructor that can set all members, passed by value
     instructiont(
-      codet _code,
+      goto_instruction_codet _code,
       source_locationt __source_location,
       goto_program_instruction_typet __type,
       exprt _guard,
@@ -880,7 +881,7 @@ class goto_programt
   make_skip(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       SKIP,
       nil_exprt(),
@@ -890,7 +891,7 @@ class goto_programt
   static instructiont make_location(const source_locationt &l)
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       LOCATION,
       nil_exprt(),
@@ -901,7 +902,7 @@ class goto_programt
   make_throw(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       THROW,
       nil_exprt(),
@@ -912,7 +913,7 @@ class goto_programt
   make_catch(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       CATCH,
       nil_exprt(),
@@ -924,7 +925,7 @@ class goto_programt
     const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       ASSERT,
       exprt(g),
@@ -936,11 +937,15 @@ class goto_programt
     const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
+      l,
+      ASSUME,
+      g,
+      {});
   }
 
   static instructiont make_other(
-    const codet &_code,
+    const goto_instruction_codet &_code,
     const source_locationt &l = source_locationt::nil())
   {
     return instructiont(_code, l, OTHER, nil_exprt(), {});
@@ -964,7 +969,7 @@ class goto_programt
   make_atomic_begin(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       ATOMIC_BEGIN,
       nil_exprt(),
@@ -975,7 +980,7 @@ class goto_programt
   make_atomic_end(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       ATOMIC_END,
       nil_exprt(),
@@ -986,7 +991,7 @@ class goto_programt
   make_end_function(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       END_FUNCTION,
       nil_exprt(),
@@ -999,7 +1004,7 @@ class goto_programt
   {
     PRECONDITION(_cond.type().id() == ID_bool);
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       INCOMPLETE_GOTO,
       _cond,
@@ -1010,7 +1015,7 @@ class goto_programt
   make_incomplete_goto(const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       INCOMPLETE_GOTO,
       true_exprt(),
@@ -1026,7 +1031,7 @@ class goto_programt
     const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       GOTO,
       true_exprt(),
@@ -1039,7 +1044,7 @@ class goto_programt
     const source_locationt &l = source_locationt::nil())
   {
     return instructiont(
-      static_cast<const codet &>(get_nil_irep()),
+      static_cast<const goto_instruction_codet &>(get_nil_irep()),
       l,
       GOTO,
       g,