diff --git a/FreeRTOS_DHCP.c b/FreeRTOS_DHCP.c
index 635c94e2d9..6a1c6b2d6b 100644
--- a/FreeRTOS_DHCP.c
+++ b/FreeRTOS_DHCP.c
@@ -217,8 +217,8 @@
 /*
  * Interpret message received on the DHCP socket.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint );
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint );
 
 /*
  * Generate a DHCP request packet, and send it on the DHCP socket.
@@ -966,8 +966,8 @@
  *
  * @return pdPASS: if DHCP options are received correctly; pdFAIL: Otherwise.
  */
-    _static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                              NetworkEndPoint_t * pxEndPoint )
+    static BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                             NetworkEndPoint_t * pxEndPoint )
     {
         uint8_t * pucUDPPayload;
         int32_t lBytes;
diff --git a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
index 09988fb2b4..c352711b21 100644
--- a/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
+++ b/test/cbmc/proofs/DHCP/DHCPProcessEndPoint/DHCPProcessEndPoint_harness.c
@@ -97,8 +97,8 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
 * Function Abstraction:
 * prvProcessDHCPReplies has been proved memory safe in ProcessDHCPReplies.
 ****************************************************************/
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
-                                  NetworkEndPoint_t * pxEndPoint )
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint )
 {
     return nondet_BaseType();
 }
diff --git a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json
index a401ed01ee..2f2f220b2e 100644
--- a/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json
+++ b/test/cbmc/proofs/ProcessDHCPReplies/Makefile.json
@@ -26,7 +26,7 @@
   "CBMCFLAGS": [
       # "--nondet-static",
       "--unwind 1",
-      "--unwindset memcmp.0:7,prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
+      "--unwindset memcmp.0:7,__CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies.0:{BUFFER_PAYLOAD}"
   ],
 
   "OBJS":
@@ -44,5 +44,11 @@
   [
     "CBMC_DHCPMESSAGE_HEADER_SIZE={BUFFER_HEADER}",
     "CBMC_FREERTOS_RECVFROM_BUFFER_BOUND={BUFFER_SIZE}"
+  ],
+
+  "OPT":
+  [
+    # Flag to access the static function of a file
+    "--export-file-local-symbols"
   ]
 }
diff --git a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
index 99e94dd3fd..dcf89ec451 100644
--- a/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
+++ b/test/cbmc/proofs/ProcessDHCPReplies/ProcessDHCPReplies_harness.c
@@ -13,18 +13,21 @@
 #include "FreeRTOS_UDP_IP.h"
 #include "FreeRTOS_DHCP.h"
 #include "FreeRTOS_ARP.h"
-
+#include "FreeRTOS_Routing.h"
 
 /****************************************************************
 * Signature of function under test
+* The function name (prvProcessDHCPReplies) is mangled due to the
+* use of a CBMC flag (--export-file-local-symbols) which allows us
+* to access this static function outside the source file in which
+* it is defined.
 ****************************************************************/
-
-BaseType_t prvProcessDHCPReplies( BaseType_t xExpectedMessageType );
+BaseType_t __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( BaseType_t xExpectedMessageType,
+                                                                       NetworkEndPoint_t * pxEndPoint );
 
 /****************************************************************
 * The proof for FreeRTOS_gethostbyname.
 ****************************************************************/
-
 void harness()
 {
     /* Omitting model of an unconstrained xDHCPData because xDHCPData is */
@@ -32,6 +35,12 @@ void harness()
     /* transaction id is an outgoing message */
 
     BaseType_t xExpectedMessageType;
+    NetworkEndPoint_t xEndPoint;
+
+    /* The function under test is a private (static) function called only by
+     * the TCP stack. The stack asserts that the endpoint cannot be NULL
+     * before the function under test is invoked. */
+    NetworkEndPoint_t * pxEndPoint = &xEndPoint;
 
-    prvProcessDHCPReplies( xExpectedMessageType );
+    __CPROVER_file_local_FreeRTOS_DHCP_c_prvProcessDHCPReplies( xExpectedMessageType, pxEndPoint );
 }