diff --git a/regression/goto-instrument/constant-propagation-function-call/main.c b/regression/goto-instrument/constant-propagation-function-call/main.c
new file mode 100644
index 00000000000..b9a8e69e2de
--- /dev/null
+++ b/regression/goto-instrument/constant-propagation-function-call/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+int ab, bc;
+int f(int x)
+{
+  ab = 1 + 1 + 1 + 1;
+  bc = ab + x;
+  return ab + bc;
+}
+int main()
+{
+  int a;
+  a = -4;
+  int b;
+  b = nondet();
+  a = f(a);
+  assert(!(0 <= a && a < 5 && 0 <= b && b < 5));
+}
diff --git a/regression/goto-instrument/constant-propagation-function-call/test.desc b/regression/goto-instrument/constant-propagation-function-call/test.desc
new file mode 100644
index 00000000000..21fbb5366cd
--- /dev/null
+++ b/regression/goto-instrument/constant-propagation-function-call/test.desc
@@ -0,0 +1,17 @@
+CORE
+main.c
+--constant-propagator
+^EXIT=10$
+^SIGNAL=0$
+Removing returns
+VERIFICATION FAILED
+ASSIGN main\:\:1\:\:a \:\= 4
+ASSERT ¬\(main::1::b ≥ 0\) ∨ main::1::b ≥ 5
+--
+^warning: ignoring
+ASSERT true
+--
+This tests that constants are propagated through function calls, correctly
+taking into account the return value. Constant propagation should result in
+simplifying away the conditions in the assertion on `a` but not the conditions
+on `b`.
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index b906ac07ba8..79716cd3767 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1285,6 +1285,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("constant-propagator"))
   {
     do_indirect_call_and_rtti_removal();
+    do_remove_returns();
 
     log.status() << "Propagating Constants" << messaget::eom;