diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
index 72f83eb6fc5..2e62f229354 100644
--- a/jbmc/src/java_bytecode/replace_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -160,7 +160,7 @@ static bool is_return_with_variable(
   const goto_programt::instructiont &instr,
   const irep_idt &identifier)
 {
-  if(!instr.is_return())
+  if(!instr.is_set_return_value())
   {
     return false;
   }
@@ -271,7 +271,7 @@ static goto_programt::targett check_and_replace_target(
       instr.turn_into_skip();
     });
 
-  if(target_instruction->is_return())
+  if(target_instruction->is_set_return_value())
   {
     const auto &nondet_var = target_instruction->return_value();
 
diff --git a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
index 41bc3cd8c71..06eda9b441b 100644
--- a/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
+++ b/jbmc/unit/java_bytecode/java_replace_nondet/replace_nondet.cpp
@@ -45,7 +45,7 @@ void validate_nondet_method_removed(
       }
     }
 
-    if(inst.is_return())
+    if(inst.is_set_return_value())
     {
       const auto &return_value = inst.return_value();
       if(return_value.id() == ID_side_effect)
@@ -94,7 +94,7 @@ void validate_nondets_converted(
     exprt target_expression =
       (inst.is_assign()
          ? inst.get_assign().rhs()
-         : inst.is_return() ? inst.return_value() : inst.get_code());
+         : inst.is_set_return_value() ? inst.return_value() : inst.get_code());
 
     if(
       const auto side_effect =
diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp
index 0adfe5d234b..3d09ad4ad68 100644
--- a/src/analyses/custom_bitvector_analysis.cpp
+++ b/src/analyses/custom_bitvector_analysis.cpp
@@ -540,8 +540,8 @@ void custom_bitvector_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 5ecbc57d014..d7ef73125bf 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -255,8 +255,8 @@ void escape_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp
index 4a18e65e6e9..80c6ae21e55 100644
--- a/src/analyses/global_may_alias.cpp
+++ b/src/analyses/global_may_alias.cpp
@@ -134,8 +134,8 @@ void global_may_alias_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index d1254979b1f..6ec2e381a2a 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -2032,7 +2032,7 @@ void goto_checkt::goto_check(
       // the call might invalidate any assertion
       assertions.clear();
     }
-    else if(i.is_return())
+    else if(i.is_set_return_value())
     {
       check(i.return_value());
       // the return value invalidate any assertion
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index b822f7162c5..2f438abdfca 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -771,7 +771,7 @@ void goto_rw(
       target->get_condition());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     rw_set.get_objects_rec(
       function, target, rw_range_sett::get_modet::READ, target->return_value());
     break;
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 6516cdcb3c5..9d34cc780eb 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -115,8 +115,8 @@ void interval_domaint::transform(
   case THROW:
     DATA_INVARIANT(false, "Exceptions must be removed before analysis");
     break;
-  case RETURN:
-    DATA_INVARIANT(false, "Returns must be removed before analysis");
+  case SET_RETURN_VALUE:
+    DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
     break;
   case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
   case ATOMIC_END:   // Ignoring is a valid over-approximation
diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp
index 8656278e3bc..6d7a588ace8 100644
--- a/src/analyses/invariant_set_domain.cpp
+++ b/src/analyses/invariant_set_domain.cpp
@@ -50,11 +50,11 @@ void invariant_set_domaint::transform(
     }
     break;
 
-  case RETURN:
-    // ignore
-    break;
+    case SET_RETURN_VALUE:
+      // ignore
+      break;
 
-  case ASSIGN:
+    case ASSIGN:
     {
       const code_assignt &assignment = from_l->get_assign();
       invariant_set.assignment(assignment.lhs(), assignment.rhs());
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index e6bc737c0f1..f9146f5ebfb 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -307,9 +307,9 @@ void local_bitvector_analysist::build()
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
 #endif
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
       break;
 #endif
     case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp
index 6ef4cd845c7..92de012b634 100644
--- a/src/analyses/local_cfg.cpp
+++ b/src/analyses/local_cfg.cpp
@@ -61,7 +61,7 @@ void local_cfgt::build(const goto_programt &goto_program)
       break; // no successor
 
     case CATCH:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case ATOMIC_BEGIN:
     case ATOMIC_END:
     case LOCATION:
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index a4703f737f0..e82fda8d231 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -423,9 +423,9 @@ void local_may_aliast::build(const goto_functiont &goto_function)
     case THROW:
       DATA_INVARIANT(false, "Exceptions must be removed before analysis");
       break;
-    case RETURN:
+    case SET_RETURN_VALUE:
 #if 0
-      DATA_INVARIANT(false, "Returns must be removed before analysis");
+      DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
 #endif
       break;
     case GOTO:         // Ignoring the guard is a valid over-approximation
diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp
index b8a3f308bb8..178a11ab04b 100644
--- a/src/analyses/local_safe_pointers.cpp
+++ b/src/analyses/local_safe_pointers.cpp
@@ -116,7 +116,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program)
     case ASSERT:
     case SKIP:
     case LOCATION:
-    case RETURN:
+    case SET_RETURN_VALUE:
     case THROW:
     case CATCH:
     case END_FUNCTION:
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index a44023486b9..b6dc242c979 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/src/analyses/uncaught_exceptions_analysis.cpp
@@ -132,7 +132,7 @@ void uncaught_exceptions_domaint::transform(
   case DEAD:   // Safe to ignore in this context
   case ASSIGN: // Safe to ignore in this context
     break;
-  case RETURN:
+  case SET_RETURN_VALUE:
 #if 0
     DATA_INVARIANT(false, "Returns must be removed before analysis");
 #endif
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
index f47f75e43ad..2be28ef0088 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
@@ -140,8 +140,8 @@ void variable_sensitivity_domaint::transform(
     // Can ignore
     break;
 
-  case RETURN:
-    throw "return instructions should be removed first";
+  case SET_RETURN_VALUE:
+    throw "the SET_RETURN_VALUE instructions should be removed first";
 
   case START_THREAD:
   case END_THREAD:
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
index 381e468bb65..072ddbbcb41 100644
--- a/src/goto-instrument/dot.cpp
+++ b/src/goto-instrument/dot.cpp
@@ -155,10 +155,9 @@ void dott::write_dot_subgraph(
         function_calls.push_back(
           std::pair<std::string, exprt>(ss.str(), function_call.function()));
       }
-      else if(it->is_assign() ||
-              it->is_decl() ||
-              it->is_return() ||
-              it->is_other())
+      else if(
+        it->is_assign() || it->is_decl() || it->is_set_return_value() ||
+        it->is_other())
       {
         std::string t = from_expr(ns, function_id, it->get_code());
         while(t[ t.size()-1 ]=='\n')
diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp
index 169ca694d5a..a1d8c853cfd 100644
--- a/src/goto-instrument/function.cpp
+++ b/src/goto-instrument/function.cpp
@@ -125,7 +125,7 @@ void function_exit(
 
     Forall_goto_program_instructions(i_it, body)
     {
-      if(i_it->is_return())
+      if(i_it->is_set_return_value())
       {
         goto_programt::instructiont call = goto_programt::make_function_call(
           function_to_call(goto_model.symbol_table, id, gf_entry.first));
@@ -142,17 +142,17 @@ void function_exit(
     assert(last->is_end_function());
 
     // is there already a return?
-    bool has_return=false;
+    bool has_set_return_value = false;
 
     if(last!=body.instructions.begin())
     {
       goto_programt::targett before_last=last;
       --before_last;
-      if(before_last->is_return())
-        has_return=true;
+      if(before_last->is_set_return_value())
+        has_set_return_value = true;
     }
 
-    if(!has_return)
+    if(!has_set_return_value)
     {
       goto_programt::instructiont call = goto_programt::make_function_call(
         function_to_call(goto_model.symbol_table, id, gf_entry.first));
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 7b81a8e7b5b..335ab389f02 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -180,8 +180,8 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
     case ASSIGN:
       return convert_assign(target, upper_bound, dest);
 
-    case RETURN:
-      return convert_return(target, upper_bound, dest);
+    case SET_RETURN_VALUE:
+      return convert_set_return_value(target, upper_bound, dest);
 
     case DECL:
       return convert_decl(target, upper_bound, dest);
@@ -410,7 +410,7 @@ void goto_program2codet::convert_assign_rec(
     dest.add(assign);
 }
 
-goto_programt::const_targett goto_program2codet::convert_return(
+goto_programt::const_targett goto_program2codet::convert_set_return_value(
   goto_programt::const_targett target,
   goto_programt::const_targett upper_bound,
   code_blockt &dest)
diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h
index 4f9082b2454..911b4c5eb9e 100644
--- a/src/goto-instrument/goto_program2code.h
+++ b/src/goto-instrument/goto_program2code.h
@@ -141,7 +141,7 @@ class goto_program2codet
 
   void convert_assign_rec(const code_assignt &assign, code_blockt &dest);
 
-  goto_programt::const_targett convert_return(
+  goto_programt::const_targett convert_set_return_value(
     goto_programt::const_targett target,
     goto_programt::const_targett upper_bound,
     code_blockt &dest);
diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp
index 237590b881b..d3f32f4e13a 100644
--- a/src/goto-instrument/points_to.cpp
+++ b/src/goto-instrument/points_to.cpp
@@ -58,7 +58,7 @@ bool points_tot::transform(const cfgt::nodet &e)
 
   switch(instruction.type)
   {
-  case RETURN:
+  case SET_RETURN_VALUE:
     // TODO
     break;
 
diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp
index df3e8a2e518..31c7fe9927f 100644
--- a/src/goto-instrument/wmm/goto2graph.cpp
+++ b/src/goto-instrument/wmm/goto2graph.cpp
@@ -260,7 +260,7 @@ void instrumentert::cfg_visitort::visit_cfg_function(
       ); // NOLINT(whitespace/parens)
     }
 #ifdef CONTEXT_INSENSITIVE
-    else if(instruction.is_return())
+    else if(instruction.is_set_return_value())
     {
       visit_cfg_propagate(i_it);
       add_all_pos(it, out_nodes[function_id], in_pos[i_it]);
@@ -1227,13 +1227,10 @@ void inline instrumentert::add_instr_to_interleaving(
   goto_programt::instructionst::iterator it,
   goto_programt &interleaving)
 {
-  if(it->is_return() ||
-     it->is_throw() ||
-     it->is_catch() ||
-     it->is_skip() ||
-     it->is_dead() ||
-     it->is_start_thread() ||
-     it->is_end_thread())
+  if(
+    it->is_set_return_value() || it->is_throw() || it->is_catch() ||
+    it->is_skip() || it->is_dead() || it->is_start_thread() ||
+    it->is_end_thread())
     return;
 
   if(it->is_atomic_begin() ||
diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h
index a2cc605ace6..83247e9b9fa 100644
--- a/src/goto-programs/cfg.h
+++ b/src/goto-programs/cfg.h
@@ -507,7 +507,7 @@ void cfg_baset<T, P, I>::compute_edges(
   case ASSIGN:
   case ASSERT:
   case OTHER:
-  case RETURN:
+  case SET_RETURN_VALUE:
   case SKIP:
   case LOCATION:
   case ATOMIC_BEGIN:
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index fc8c7172b64..490c2e65037 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -119,7 +119,7 @@ void goto_convert_functionst::add_return(
       }
 
       // return?
-      if(last_instruction->is_return())
+      if(last_instruction->is_set_return_value())
         return;
 
       // advance if it's a 'dead' without branch target
diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp
index 9f66973c437..8b0c26b6770 100644
--- a/src/goto-programs/goto_functions.cpp
+++ b/src/goto-programs/goto_functions.cpp
@@ -138,7 +138,7 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
       {
         DATA_CHECK(
           vm,
-          !instruction.is_return(),
+          !instruction.is_set_return_value(),
           "void function should not return a value");
       }
     }
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index 534c2aaa2f0..880bca1f446 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -155,7 +155,7 @@ void goto_inlinet::replace_return(
       it!=dest.instructions.end();
       it++)
   {
-    if(it->is_return())
+    if(it->is_set_return_value())
     {
       if(lhs.is_not_nil())
       {
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index de9aec6ffb1..22b9059b4aa 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -112,10 +112,11 @@ std::ostream &goto_programt::output_instruction(
       }
       // fallthrough
     }
+
     out << "OTHER " << format(instruction.get_other());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     out << "RETURN " << format(instruction.return_value()) << '\n';
     break;
 
@@ -323,7 +324,7 @@ std::list<exprt> expressions_read(
     dest.push_back(instruction.get_condition());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     dest.push_back(instruction.return_value());
     break;
 
@@ -385,7 +386,7 @@ std::list<exprt> expressions_written(
   case CATCH:
   case THROW:
   case GOTO:
-  case RETURN:
+  case SET_RETURN_VALUE:
   case DEAD:
   case DECL:
   case ATOMIC_BEGIN:
@@ -501,7 +502,7 @@ std::string as_string(
     }
     return result;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
   case OTHER:
   case DECL:
   case DEAD:
@@ -883,11 +884,11 @@ void goto_programt::instructiont::validate(
     break;
   case ATOMIC_END:
     break;
-  case RETURN:
+  case SET_RETURN_VALUE:
     DATA_CHECK_WITH_DIAGNOSTICS(
       vm,
       code.get_statement() == ID_return,
-      "return instruction should contain a return statement",
+      "SET_RETURN_VALUE instruction should contain a return statement",
       source_location);
     break;
   case ASSIGN:
@@ -961,7 +962,7 @@ void goto_programt::instructiont::transform(
     }
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
   {
     auto new_return_value = f(return_value());
     if(new_return_value.has_value())
@@ -1063,7 +1064,7 @@ void goto_programt::instructiont::apply(
       f(to_code_expression(get_other()).expression());
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     f(return_value());
     break;
 
@@ -1186,8 +1187,8 @@ std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
   case ATOMIC_END:
     out << "ATOMIC_END";
     break;
-  case RETURN:
-    out << "RETURN";
+  case SET_RETURN_VALUE:
+    out << "SET_RETURN_VALUE";
     break;
   case ASSIGN:
     out << "ASSIGN";
diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h
index 8312999ae5a..81168c0c823 100644
--- a/src/goto-programs/goto_program.h
+++ b/src/goto-programs/goto_program.h
@@ -30,25 +30,25 @@ enum class validation_modet;
 enum goto_program_instruction_typet
 {
   NO_INSTRUCTION_TYPE = 0,
-  GOTO = 1,            // branch, possibly guarded
-  ASSUME = 2,          // non-failing guarded self loop
-  ASSERT = 3,          // assertions
-  OTHER = 4,           // anything else
-  SKIP = 5,            // just advance the PC
-  START_THREAD = 6,    // spawns an asynchronous thread
-  END_THREAD = 7,      // end the current thread
-  LOCATION = 8,        // semantically like SKIP
-  END_FUNCTION = 9,    // exit point of a function
-  ATOMIC_BEGIN = 10,   // marks a block without interleavings
-  ATOMIC_END = 11,     // end of a block without interleavings
-  RETURN = 12,         // set function return value (no control-flow change)
-  ASSIGN = 13,         // assignment lhs:=rhs
-  DECL = 14,           // declare a local variable
-  DEAD = 15,           // marks the end-of-live of a local variable
-  FUNCTION_CALL = 16,  // call a function
-  THROW = 17,          // throw an exception
-  CATCH = 18,          // push, pop or enter an exception handler
-  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
+  GOTO = 1,              // branch, possibly guarded
+  ASSUME = 2,            // non-failing guarded self loop
+  ASSERT = 3,            // assertions
+  OTHER = 4,             // anything else
+  SKIP = 5,              // just advance the PC
+  START_THREAD = 6,      // spawns an asynchronous thread
+  END_THREAD = 7,        // end the current thread
+  LOCATION = 8,          // semantically like SKIP
+  END_FUNCTION = 9,      // exit point of a function
+  ATOMIC_BEGIN = 10,     // marks a block without interleavings
+  ATOMIC_END = 11,       // end of a block without interleavings
+  SET_RETURN_VALUE = 12, // set function return value (no control-flow change)
+  ASSIGN = 13,           // assignment lhs:=rhs
+  DECL = 14,             // declare a local variable
+  DEAD = 15,             // marks the end-of-live of a local variable
+  FUNCTION_CALL = 16,    // call a function
+  THROW = 17,            // throw an exception
+  CATCH = 18,            // push, pop or enter an exception handler
+  INCOMPLETE_GOTO = 19   // goto where target is yet to be determined
 };
 
 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
@@ -111,9 +111,9 @@ class goto_programt
   ///     goto `targets` if and only if `guard` is true.
   ///     More than one target is deprecated.  Its semantics was a
   ///     non-deterministic choice.
-  /// - RETURN:
-  ///     Set the value returned by `code` (which shall be either nil or an
-  ///     instance of code_returnt) and then jump to the end of the function.
+  /// - SET_RETURN_VALUE:
+  ///     Set the value returned by `return_value()`.  The control flow is
+  ///     not altered.
   ///     Many analysis tools remove these instructions before they start.
   /// - DECL:
   ///     Introduces a symbol denoted by the field `code` (an instance of
@@ -317,29 +317,29 @@ class goto_programt
     DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
     const code_returnt &get_return() const
     {
-      PRECONDITION(is_return());
+      PRECONDITION(is_set_return_value());
       return to_code_return(code);
     }
 
-    /// Get the return value of a RETURN instruction
+    /// Get the return value of a SET_RETURN_VALUE instruction
     const exprt &return_value() const
     {
-      PRECONDITION(is_return());
+      PRECONDITION(is_set_return_value());
       return to_code_return(code).return_value();
     }
 
-    /// Get the return value of a RETURN instruction
+    /// Get the return value of a SET_RETURN_VALUE instruction
     exprt &return_value()
     {
-      PRECONDITION(is_return());
+      PRECONDITION(is_set_return_value());
       return to_code_return(code).return_value();
     }
 
-    /// Set the return statement for READ
+    /// Set the return statement for SET_RETURN_VALUE
     DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
     void set_return(code_returnt c)
     {
-      PRECONDITION(is_return());
+      PRECONDITION(is_set_return_value());
       code = std::move(c);
     }
 
@@ -467,28 +467,27 @@ class goto_programt
       type = GOTO;
     }
 
-    bool is_goto         () const { return type==GOTO;          }
-    bool is_return       () const { return type==RETURN;        }
-    bool is_assign       () const { return type==ASSIGN;        }
-    bool is_function_call() const { return type==FUNCTION_CALL; }
-    bool is_throw        () const { return type==THROW;         }
-    bool is_catch        () const { return type==CATCH;         }
-    bool is_skip         () const { return type==SKIP;          }
-    bool is_location     () const { return type==LOCATION;      }
-    bool is_other        () const { return type==OTHER;         }
-    bool is_decl         () const { return type==DECL;          }
-    bool is_dead         () const { return type==DEAD;          }
-    bool is_assume       () const { return type==ASSUME;        }
-    bool is_assert       () const { return type==ASSERT;        }
-    bool is_atomic_begin () const { return type==ATOMIC_BEGIN;  }
-    bool is_atomic_end   () const { return type==ATOMIC_END;    }
-    bool is_start_thread () const { return type==START_THREAD;  }
-    bool is_end_thread   () const { return type==END_THREAD;    }
-    bool is_end_function () const { return type==END_FUNCTION;  }
-    bool is_incomplete_goto() const
-    {
-      return type == INCOMPLETE_GOTO;
-    }
+    // clang-format off
+    bool is_goto            () const { return type == GOTO;             }
+    bool is_set_return_value() const { return type == SET_RETURN_VALUE; }
+    bool is_assign          () const { return type == ASSIGN;           }
+    bool is_function_call   () const { return type == FUNCTION_CALL;    }
+    bool is_throw           () const { return type == THROW;            }
+    bool is_catch           () const { return type == CATCH;            }
+    bool is_skip            () const { return type == SKIP;             }
+    bool is_location        () const { return type == LOCATION;         }
+    bool is_other           () const { return type == OTHER;            }
+    bool is_decl            () const { return type == DECL;             }
+    bool is_dead            () const { return type == DEAD;             }
+    bool is_assume          () const { return type == ASSUME;           }
+    bool is_assert          () const { return type == ASSERT;           }
+    bool is_atomic_begin    () const { return type == ATOMIC_BEGIN;     }
+    bool is_atomic_end      () const { return type == ATOMIC_END;       }
+    bool is_start_thread    () const { return type == START_THREAD;     }
+    bool is_end_thread      () const { return type == END_THREAD;       }
+    bool is_end_function    () const { return type == END_FUNCTION;     }
+    bool is_incomplete_goto () const { return type == INCOMPLETE_GOTO;  }
+    // clang-format on
 
     instructiont():
       instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
@@ -849,14 +848,14 @@ class goto_programt
   static instructiont
   make_return(const source_locationt &l = source_locationt::nil())
   {
-    return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
+    return instructiont(code_returnt(), l, SET_RETURN_VALUE, nil_exprt(), {});
   }
 
   static instructiont make_return(
     code_returnt c,
     const source_locationt &l = source_locationt::nil())
   {
-    return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
+    return instructiont(std::move(c), l, SET_RETURN_VALUE, nil_exprt(), {});
   }
 
   static instructiont
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 74e771d0270..adedd00b4a9 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -570,10 +570,11 @@ void show_full_goto_trace(
       break;
 
     case goto_trace_stept::typet::ASSIGNMENT:
-      if(step.pc->is_assign() ||
-         step.pc->is_return() || // returns have a lhs!
-         step.pc->is_function_call() ||
-         (step.pc->is_other() && step.full_lhs.is_not_nil()))
+      if(
+        step.pc->is_assign() ||
+        step.pc->is_set_return_value() || // returns have a lhs!
+        step.pc->is_function_call() ||
+        (step.pc->is_other() && step.full_lhs.is_not_nil()))
       {
         if(prev_step_nr!=step.step_nr || first_step)
         {
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index ba57b5a9ec0..cf76fe390d5 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -291,10 +291,10 @@ void interpretert::step()
     trace_step.type=goto_trace_stept::typet::FUNCTION_RETURN;
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     trace_step.type=goto_trace_stept::typet::FUNCTION_RETURN;
     if(call_stack.empty())
-      throw "RETURN without call"; // NOLINT(readability/throw)
+      throw "SET_RETURN_VALUE without call"; // NOLINT(readability/throw)
 
     if(call_stack.top().return_value_address != 0)
     {
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 3e56e3afc80..317c3e32966 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -115,7 +115,7 @@ void remove_returnst::replace_returns(
 
   for(auto &instruction : goto_program.instructions)
   {
-    if(instruction.is_return())
+    if(instruction.is_set_return_value())
     {
       INVARIANT(
         instruction.get_code().operands().size() == 1,
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index 21730daa7cd..611a47a3521 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -484,7 +484,7 @@ goto_programt::targett string_abstractiont::abstract(
     abstract_function_call(it);
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     // use remove_returns
     UNREACHABLE;
     break;
diff --git a/src/goto-programs/validate_goto_model.cpp b/src/goto-programs/validate_goto_model.cpp
index 63f45a91a57..ac2fe9b229b 100644
--- a/src/goto-programs/validate_goto_model.cpp
+++ b/src/goto-programs/validate_goto_model.cpp
@@ -126,7 +126,9 @@ void validate_goto_modelt::check_returns_removed()
     for(const auto &instr : goto_function.body.instructions)
     {
       DATA_CHECK(
-        vm, !instr.is_return(), "no return instructions should be present");
+        vm,
+        !instr.is_set_return_value(),
+        "no SET_RETURN_VALUE instructions should be present");
 
       if(instr.is_function_call())
       {
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index baadee745b5..e88b6d128d5 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -660,7 +660,7 @@ void goto_symext::execute_next_instruction(
     symex_transition(state);
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
     // This case should have been removed by return-value removal
     UNREACHABLE;
     break;
diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp
index 505687b7ea4..2e669bb8c5c 100644
--- a/src/pointer-analysis/goto_program_dereference.cpp
+++ b/src/pointer-analysis/goto_program_dereference.cpp
@@ -225,7 +225,7 @@ void goto_program_dereferencet::dereference_instruction(
 
     i.set_function_call(function_call);
   }
-  else if(i.is_return())
+  else if(i.is_set_return_value())
   {
     dereference_expr(i.return_value(), checks_only);
   }
diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h
index 02942740789..73105124a3b 100644
--- a/src/pointer-analysis/value_set_domain.h
+++ b/src/pointer-analysis/value_set_domain.h
@@ -83,7 +83,7 @@ void value_set_domain_templatet<VST>::transform(
   }
 
   // Note intentional fall-through here:
-  case RETURN:
+  case SET_RETURN_VALUE:
   case OTHER:
   case ASSIGN:
   case DECL:
diff --git a/src/pointer-analysis/value_set_domain_fi.cpp b/src/pointer-analysis/value_set_domain_fi.cpp
index 789e50fdd31..3728701e98e 100644
--- a/src/pointer-analysis/value_set_domain_fi.cpp
+++ b/src/pointer-analysis/value_set_domain_fi.cpp
@@ -40,7 +40,7 @@ bool value_set_domain_fit::transform(
     value_set.do_end_function(get_return_lhs(to_l), ns);
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
   case OTHER:
   case ASSIGN:
     value_set.apply_code(from_l->get_code(), ns);
diff --git a/src/solvers/solver_hardness.cpp b/src/solvers/solver_hardness.cpp
index 6ef843c8821..f276fa2cdd5 100644
--- a/src/solvers/solver_hardness.cpp
+++ b/src/solvers/solver_hardness.cpp
@@ -267,7 +267,10 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc)
     }
     break;
 
-  case RETURN:
+  case SET_RETURN_VALUE:
+    out << "SET RETURN VALUE" << format(instruction.return_value());
+    break;
+
   case OTHER:
   case DECL:
   case DEAD: