diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 126b23a1ee3..85e0debb0df 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -54,10 +54,11 @@ class remove_returnst
   void undo_function_calls(
     goto_programt &goto_program);
 
-  symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);
+  optionalt<symbol_exprt>
+  get_or_create_return_value_symbol(const irep_idt &function_id);
 };
 
-symbol_exprt
+optionalt<symbol_exprt>
 remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
 {
   const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
@@ -69,7 +70,7 @@ remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
   const typet &return_type = to_code_type(function_symbol.type).return_type();
 
   if(return_type == empty_typet())
-    return symbol_exprt();
+    return {};
 
   auxiliary_symbolt new_symbol;
   new_symbol.is_static_lifetime = true;
@@ -103,7 +104,7 @@ void remove_returnst::replace_returns(
     return;
 
   // add return_value symbol to symbol_table, if not already created:
-  symbol_exprt return_symbol = get_or_create_return_value_symbol(function_id);
+  const auto return_symbol = get_or_create_return_value_symbol(function_id);
 
   // look up the function symbol
   symbolt &function_symbol = *symbol_table.get_writeable(function_id);
@@ -122,11 +123,16 @@ void remove_returnst::replace_returns(
         i_it->code.operands().size() == 1,
         "return instructions should have one operand");
 
-      // replace "return x;" by "fkt#return_value=x;"
-      code_assignt assignment(return_symbol, i_it->code.op0());
+      if(return_symbol.has_value())
+      {
+        // replace "return x;" by "fkt#return_value=x;"
+        code_assignt assignment(*return_symbol, i_it->code.op0());
 
-      // now turn the `return' into `assignment'
-      i_it->make_assignment(assignment);
+        // now turn the `return' into `assignment'
+        i_it->make_assignment(assignment);
+      }
+      else
+        i_it->make_skip();
     }
   }
 }
@@ -153,7 +159,7 @@ void remove_returnst::do_function_calls(
       const irep_idt function_id =
         to_symbol_expr(function_call.function()).get_identifier();
 
-      symbol_exprt return_value;
+      optionalt<symbol_exprt> return_value;
       typet old_return_type;
       bool is_stub = function_is_stub(function_id);
 
@@ -169,9 +175,9 @@ void remove_returnst::do_function_calls(
         // To simplify matters, create its return-value global now (if not
         // already done), and use that to determine its true return type.
         return_value = get_or_create_return_value_symbol(function_id);
-        if(return_value == symbol_exprt()) // really void-typed?
+        if(!return_value.has_value()) // really void-typed?
           continue;
-        old_return_type = return_value.type();
+        old_return_type = return_value->type();
       }
 
       // Do we return anything?
@@ -194,7 +200,7 @@ void remove_returnst::do_function_calls(
             // from the return type in the declaration.  We therefore do a
             // cast.
             rhs = typecast_exprt::conditional_cast(
-              return_value, function_call.lhs().type());
+              *return_value, function_call.lhs().type());
           }
           else
             rhs = side_effect_expr_nondett(
@@ -214,7 +220,7 @@ void remove_returnst::do_function_calls(
             goto_programt::targett t_d=goto_program.insert_after(t_a);
             t_d->make_dead();
             t_d->source_location=i_it->source_location;
-            t_d->code = code_deadt(return_value);
+            t_d->code = code_deadt(*return_value);
             t_d->function=i_it->function;
           }
         }
diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp
index 8b0e96ac0d9..cb603f3a836 100644
--- a/src/goto-programs/remove_virtual_functions.cpp
+++ b/src/goto-programs/remove_virtual_functions.cpp
@@ -54,7 +54,7 @@ class remove_virtual_functionst
     function_call_resolvert;
   void get_child_functions_rec(
     const irep_idt &,
-    const symbol_exprt &,
+    const optionalt<symbol_exprt> &,
     const irep_idt &,
     dispatch_table_entriest &,
     dispatch_table_entries_mapt &,
@@ -166,7 +166,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   if(functions.size()==1 &&
      fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)
   {
-    if(functions.begin()->symbol_expr==symbol_exprt())
+    if(!functions.front().symbol_expr.has_value())
     {
       target->make_skip();
       remove_skip(goto_program, target, next_target);
@@ -174,7 +174,9 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
     else
     {
       create_static_function_call(
-        to_code_function_call(target->code), functions.front().symbol_expr, ns);
+        to_code_function_call(target->code),
+        *functions.front().symbol_expr,
+        ns);
     }
     return next_target;
   }
@@ -195,7 +197,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   goto_programt new_code_gotos;
 
   exprt this_expr=code.arguments()[0];
-  const auto &last_function_symbol=functions.back().symbol_expr;
 
   const typet &this_type=this_expr.type();
   INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer");
@@ -219,26 +220,29 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
 
   // get initial identifier for grouping
   INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
+  const auto &last_function_symbol = functions.back().symbol_expr;
 
   std::map<irep_idt, goto_programt::targett> calls;
   // Note backwards iteration, to get the fallback candidate first.
   for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
   {
     const auto &fun=*it;
-    auto insertit=calls.insert(
-      {fun.symbol_expr.get_identifier(), goto_programt::targett()});
+    irep_idt id_or_empty = fun.symbol_expr.has_value()
+                             ? fun.symbol_expr->get_identifier()
+                             : irep_idt();
+    auto insertit = calls.insert({id_or_empty, goto_programt::targett()});
 
     // Only create one call sequence per possible target:
     if(insertit.second)
     {
       goto_programt::targett t1=new_code_calls.add_instruction();
       t1->source_location=vcall_source_loc;
-      if(!fun.symbol_expr.get_identifier().empty())
+      if(fun.symbol_expr.has_value())
       {
       // call function
         t1->make_function_call(code);
         create_static_function_call(
-          to_code_function_call(t1->code), fun.symbol_expr, ns);
+          to_code_function_call(t1->code), *fun.symbol_expr, ns);
       }
       else
       {
@@ -257,9 +261,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
     }
 
     // Fall through to the default callee if possible:
-    if(fallback_action ==
-       virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
-       fun.symbol_expr == last_function_symbol)
+    if(
+      fallback_action ==
+        virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
+      fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
+      (!fun.symbol_expr.has_value() ||
+       *fun.symbol_expr == *last_function_symbol))
     {
       // Nothing to do
     }
@@ -271,8 +278,11 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
 
       // If the previous GOTO goes to the same callee, join it
       // (e.g. turning IF x GOTO y into IF x || z GOTO y)
-      if(it != functions.crbegin() &&
-         std::prev(it)->symbol_expr == fun.symbol_expr)
+      if(
+        it != functions.crbegin() &&
+        std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
+        (!fun.symbol_expr.has_value() ||
+         *(std::prev(it)->symbol_expr) == *fun.symbol_expr))
       {
         INVARIANT(
           !new_code_gotos.empty(),
@@ -337,7 +347,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
 /// \param resolve_function_call`: function to resolve abstract method call
 void remove_virtual_functionst::get_child_functions_rec(
   const irep_idt &this_id,
-  const symbol_exprt &last_method_defn,
+  const optionalt<symbol_exprt> &last_method_defn,
   const irep_idt &component_name,
   dispatch_table_entriest &functions,
   dispatch_table_entries_mapt &entry_map,
@@ -354,9 +364,10 @@ void remove_virtual_functionst::get_child_functions_rec(
     auto it = entry_map.find(child);
     if(
       it != entry_map.end() &&
-      !has_prefix(
-        id2string(it->second.symbol_expr.get_identifier()),
-        "java::java.lang.Object"))
+      (!it->second.symbol_expr.has_value() ||
+       !has_prefix(
+         id2string(it->second.symbol_expr->get_identifier()),
+         "java::java.lang.Object")))
     {
       continue;
     }
@@ -365,13 +376,13 @@ void remove_virtual_functionst::get_child_functions_rec(
     if(method.is_not_nil())
     {
       function.symbol_expr=to_symbol_expr(method);
-      function.symbol_expr.set(ID_C_class, child);
+      function.symbol_expr->set(ID_C_class, child);
     }
     else
     {
       function.symbol_expr=last_method_defn;
     }
-    if(function.symbol_expr == symbol_exprt())
+    if(!function.symbol_expr.has_value())
     {
       const resolve_inherited_componentt::inherited_componentt
         &resolved_call = resolve_function_call(child, component_name);
@@ -383,12 +394,12 @@ void remove_virtual_functionst::get_child_functions_rec(
             resolved_call.get_full_component_identifier());
 
         function.symbol_expr = called_symbol.symbol_expr();
-        function.symbol_expr.set(
+        function.symbol_expr->set(
           ID_C_class, resolved_call.get_class_identifier());
       }
     }
     functions.push_back(function);
-    entry_map.insert({child, function});
+    entry_map.emplace(child, function);
 
     get_child_functions_rec(
       child,
@@ -426,7 +437,8 @@ void remove_virtual_functionst::get_functions(
   const resolve_inherited_componentt::inherited_componentt
     &resolved_call = get_virtual_call_target(class_id, function_name, false);
 
-  dispatch_table_entryt root_function;
+  // might be an abstract function
+  dispatch_table_entryt root_function(class_id);
 
   if(resolved_call.is_valid())
   {
@@ -436,14 +448,9 @@ void remove_virtual_functionst::get_functions(
       symbol_table.lookup_ref(resolved_call.get_full_component_identifier());
 
     root_function.symbol_expr=called_symbol.symbol_expr();
-    root_function.symbol_expr.set(
+    root_function.symbol_expr->set(
       ID_C_class, resolved_call.get_class_identifier());
   }
-  else
-  {
-    // No definition here; this is an abstract function.
-    root_function.class_id=class_id;
-  }
 
   // iterate over all children, transitively
   dispatch_table_entries_mapt entry_map;
@@ -455,7 +462,7 @@ void remove_virtual_functionst::get_functions(
     entry_map,
     resolve_function_call);
 
-  if(root_function.symbol_expr!=symbol_exprt())
+  if(root_function.symbol_expr.has_value())
     functions.push_back(root_function);
 
   // Sort for the identifier of the function call symbol expression, grouping
@@ -465,20 +472,21 @@ void remove_virtual_functionst::get_functions(
   std::sort(
     functions.begin(),
     functions.end(),
-    [](const dispatch_table_entryt &a, dispatch_table_entryt &b)
-    {
-      if(
-        has_prefix(
-          id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
+    [](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
+      irep_idt a_id = a.symbol_expr.has_value()
+                        ? a.symbol_expr->get_identifier()
+                        : irep_idt();
+      irep_idt b_id = b.symbol_expr.has_value()
+                        ? b.symbol_expr->get_identifier()
+                        : irep_idt();
+
+      if(has_prefix(id2string(a_id), "java::java.lang.Object"))
         return false;
-      else if(
-        has_prefix(
-          id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
+      else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
         return true;
       else
       {
-        int cmp = a.symbol_expr.get_identifier().compare(
-          b.symbol_expr.get_identifier());
+        int cmp = a_id.compare(b_id);
         if(cmp == 0)
           return a.class_id < b.class_id;
         else
diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h
index b47854e63f8..69b8f243ca3 100644
--- a/src/goto-programs/remove_virtual_functions.h
+++ b/src/goto-programs/remove_virtual_functions.h
@@ -15,6 +15,7 @@ Date: April 2016
 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
 #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
 
+#include <util/optional.h>
 #include <util/std_expr.h>
 
 #include "class_hierarchy.h"
@@ -52,13 +53,35 @@ enum class virtual_dispatch_fallback_actiont
 
 class dispatch_table_entryt
 {
- public:
-  dispatch_table_entryt() = default;
-  explicit dispatch_table_entryt(const irep_idt &_class_id) :
-    class_id(_class_id)
-  {}
-
-  symbol_exprt symbol_expr;
+public:
+  explicit dispatch_table_entryt(const irep_idt &_class_id)
+    : symbol_expr(), class_id(_class_id)
+  {
+  }
+
+#if defined(__GNUC__) && __GNUC__ < 7
+  // GCC up to version 6.5 warns about irept::data being used uninitialized upon
+  // the move triggered by std::sort; using operator= works around this
+  dispatch_table_entryt(dispatch_table_entryt &&other)
+  {
+    symbol_expr = other.symbol_expr;
+    class_id = other.class_id;
+  }
+
+  dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
+  {
+    symbol_expr = other.symbol_expr;
+    class_id = other.class_id;
+    return *this;
+  }
+
+  dispatch_table_entryt(const dispatch_table_entryt &other)
+    : symbol_expr(other.symbol_expr), class_id(other.class_id)
+  {
+  }
+#endif
+
+  optionalt<symbol_exprt> symbol_expr;
   irep_idt class_id;
 };