diff --git a/regression/goto-instrument/generate-function-body-nondet-return-const/main.c b/regression/goto-instrument/generate-function-body-nondet-return-const/main.c
new file mode 100644
index 00000000000..c1e66dfe226
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-const/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+const int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-const/test.desc b/regression/goto-instrument/generate-function-body-nondet-return-const/test.desc
new file mode 100644
index 00000000000..441ac40d68a
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-const/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/main.c b/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/main.c
new file mode 100644
index 00000000000..9baecdf7567
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/main.c
@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int **func();
+
+void main()
+{
+  int **p = func();
+
+  assert(p != NULL);
+  assert(*p != NULL);
+
+  assert(**p == 0);
+  assert(**p != 0);
+}
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/test.desc b/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/test.desc
new file mode 100644
index 00000000000..7a90ef15385
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-double-pointer/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 5
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.2\] line \d+ assertion \*p != .*(0|(NULL))\)?: SUCCESS
+\[main.assertion.3\] line \d+ assertion \*\*p == 0: FAILURE
+\[main.assertion.4\] line \d+ assertion \*\*p != 0: FAILURE
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-simple/main.c b/regression/goto-instrument/generate-function-body-nondet-return-simple/main.c
new file mode 100644
index 00000000000..6cf910991c6
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-simple/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int func();
+
+void main()
+{
+  assert(func() == 0);
+  assert(func() != 0);
+}
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-simple/test.desc b/regression/goto-instrument/generate-function-body-nondet-return-simple/test.desc
new file mode 100644
index 00000000000..441ac40d68a
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-simple/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return
+^SIGNAL=0$
+\[main.assertion.1\] line \d+ assertion func\(\) == 0: FAILURE
+\[main.assertion.2\] line \d+ assertion func\(\) != 0: FAILURE
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/main.c b/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/main.c
new file mode 100644
index 00000000000..040cc869960
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/main.c
@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct st
+{
+  struct st *next;
+  int data;
+} st_t;
+
+st_t dummy;
+
+st_t *func();
+
+void main()
+{
+  st_t *st = func();
+
+  assert(st != NULL);
+
+  assert(st->next != NULL);
+  assert(st->next->next != NULL);
+  assert(st->next->next->next == NULL);
+
+  assert(st != &dummy);
+  assert(st->next != &dummy);
+  assert(st->next->next != &dummy);
+}
diff --git a/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/test.desc b/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/test.desc
new file mode 100644
index 00000000000..b1252a108a3
--- /dev/null
+++ b/regression/goto-instrument/generate-function-body-nondet-return-struct-simple-recursion/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--generate-function-body func --generate-function-body-options nondet-return --min-null-tree-depth 10 --max-nondet-tree-depth 3
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp
index b0dea5c7f88..b7ce2a17019 100644
--- a/src/goto-instrument/generate_function_bodies.cpp
+++ b/src/goto-instrument/generate_function_bodies.cpp
@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
 #include <util/format_expr.h>
+#include <util/fresh_symbol.h>
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
@@ -271,11 +272,46 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
 
     if(function.type.return_type() != void_typet())
     {
+      typet type(function.type.return_type());
+      type.remove(ID_C_constant);
+
+      symbolt &aux_symbol = get_fresh_aux_symbol(
+        type,
+        id2string(function_name),
+        "return_value",
+        function_symbol.location,
+        ID_C,
+        symbol_table);
+
+      aux_symbol.is_static_lifetime = false;
+
+      auto decl_instruction = add_instruction();
+      decl_instruction->make_decl();
+      decl_instruction->code = code_declt(aux_symbol.symbol_expr());
+
+      goto_programt dest;
+
+      havoc_expr_rec(
+        aux_symbol.symbol_expr(),
+        0,
+        function_symbol.location,
+        symbol_table,
+        dest);
+
+      function.body.destructive_append(dest);
+
+      exprt return_expr = typecast_exprt::conditional_cast(
+        aux_symbol.symbol_expr(), function.type.return_type());
+
       auto return_instruction = add_instruction();
       return_instruction->make_return();
-      return_instruction->code = code_returnt(side_effect_expr_nondett(
-        function.type.return_type(), function_symbol.location));
+      return_instruction->code = code_returnt(return_expr);
+
+      auto dead_instruction = add_instruction();
+      dead_instruction->make_dead();
+      dead_instruction->code = code_deadt(aux_symbol.symbol_expr());
     }
+
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();