diff --git a/regression/cbmc/return7/main.c b/regression/cbmc/return7/main.c
new file mode 100644
index 00000000000..938f06d0d84
--- /dev/null
+++ b/regression/cbmc/return7/main.c
@@ -0,0 +1,18 @@
+void a()
+{
+  // Uses the implicit signature of undefined functions: int c(void)
+  int b;
+  b = c();
+  __CPROVER_assert(b == 0, "expected to fail");
+}
+void c(void)
+{
+  // Actually... don't return anything
+  // So the results will be non-deterministic
+}
+
+int main(int argc, char **argv)
+{
+  a();
+  return 0;
+}
diff --git a/regression/cbmc/return7/test.desc b/regression/cbmc/return7/test.desc
new file mode 100644
index 00000000000..1d3f29ded69
--- /dev/null
+++ b/regression/cbmc/return7/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+Reason: Check return value
+^warning: ignoring
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 38f6567f41a..62278e631fa 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -762,6 +762,16 @@ void goto_convertt::do_function_call_symbol(
     code_function_callt function_call(lhs, function, arguments);
     function_call.add_source_location() = function.source_location();
 
+    // remove void-typed assignments, which may have been created when the
+    // front-end was unable to detect them in type checking for a lack of
+    // available declarations
+    if(
+      lhs.is_not_nil() &&
+      to_code_type(symbol->type).return_type().id() == ID_empty)
+    {
+      function_call.lhs().make_nil();
+    }
+
     copy(function_call, FUNCTION_CALL, dest);
 
     return;
@@ -1435,6 +1445,16 @@ void goto_convertt::do_function_call_symbol(
     code_function_callt function_call(lhs, function, arguments);
     function_call.add_source_location()=function.source_location();
 
+    // remove void-typed assignments, which may have been created when the
+    // front-end was unable to detect them in type checking for a lack of
+    // available declarations
+    if(
+      lhs.is_not_nil() &&
+      to_code_type(symbol->type).return_type().id() == ID_empty)
+    {
+      function_call.lhs().make_nil();
+    }
+
     copy(function_call, FUNCTION_CALL, dest);
   }
 }
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 2d47e827b75..dcdeab90ba1 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -175,10 +175,10 @@ bool remove_returnst::do_function_calls(
         optionalt<symbol_exprt> return_value;
 
         if(!is_stub)
-        {
           return_value = get_or_create_return_value_symbol(function_id);
-          CHECK_RETURN(return_value.has_value());
 
+        if(return_value.has_value())
+        {
           // The return type in the definition of the function may differ
           // from the return type in the declaration.  We therefore do a
           // cast.
@@ -199,7 +199,7 @@ bool remove_returnst::do_function_calls(
         // fry the previous assignment
         i_it->call_lhs().make_nil();
 
-        if(!is_stub)
+        if(return_value.has_value())
         {
           goto_program.insert_after(
             t_a,