diff --git a/regression/crangler/remove-static/remove_static1.c b/regression/crangler/remove-static/remove_static1.c
index 10df0a9e611..14d3eb3179b 100644
--- a/regression/crangler/remove-static/remove_static1.c
+++ b/regression/crangler/remove-static/remove_static1.c
@@ -5,6 +5,8 @@ int foo()
 
 int bar();
 
+static void foobar2();
+
 static void foobar1()
 {
 }
diff --git a/regression/crangler/remove-static/remove_static1.desc b/regression/crangler/remove-static/remove_static1.desc
index ca027e08038..e5490c134dc 100644
--- a/regression/crangler/remove-static/remove_static1.desc
+++ b/regression/crangler/remove-static/remove_static1.desc
@@ -6,3 +6,4 @@ remove_static1.json
 ^EXIT=0$
 ^SIGNAL=0$
 --
+static\s+(void\s+)?foobar[12]\(\)$
diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp
index 369bf736f8e..a92e610caa9 100644
--- a/src/crangler/c_wrangler.cpp
+++ b/src/crangler/c_wrangler.cpp
@@ -368,7 +368,7 @@ static void mangle_function(
   const c_wranglert::functiont &function_config,
   std::ostream &out)
 {
-  if(function_config.stub.has_value())
+  if(function_config.stub.has_value() && declaration.has_body())
   {
     // replace by stub
     out << function_config.stub.value();
@@ -399,6 +399,13 @@ static void mangle_function(
     for(auto &t : declaration.post_declarator)
       out << t.text;
 
+    if(!declaration.has_body())
+    {
+      for(auto &t : declaration.initializer)
+        out << t.text;
+      return;
+    }
+
     for(const auto &entry : function_config.contract)
       out << ' ' << CPROVER_PREFIX << entry.clause << '('
           << defines(entry.content) << ')';
@@ -498,8 +505,7 @@ static void mangle(
   std::ostream &out)
 {
   auto name_opt = declaration.declared_identifier();
-  if(
-    declaration.is_function() && name_opt.has_value() && declaration.has_body())
+  if(declaration.is_function() && name_opt.has_value())
   {
     for(const auto &entry : config.functions)
     {