diff --git a/source/include/FreeRTOSIPConfigDefaults.h b/source/include/FreeRTOSIPConfigDefaults.h
index 97a0b08684..1c951cf786 100644
--- a/source/include/FreeRTOSIPConfigDefaults.h
+++ b/source/include/FreeRTOSIPConfigDefaults.h
@@ -3063,8 +3063,8 @@
 #endif
 
 #ifndef FreeRTOS_debug_printf
-    #ifdef configPRINTF
-        #define FreeRTOS_debug_printf( MSG )    if( ipconfigHAS_DEBUG_PRINTF ) configPRINTF( MSG )
+    #if ( ipconfigHAS_DEBUG_PRINTF == 1 ) && defined( configPRINTF )
+        #define FreeRTOS_debug_printf( MSG )    do { configPRINTF( MSG ); } while( ipFALSE_BOOL )
     #else
         #define FreeRTOS_debug_printf( MSG )    do {} while( ipFALSE_BOOL )
     #endif
@@ -3099,8 +3099,8 @@
 #endif
 
 #ifndef FreeRTOS_printf
-    #ifdef configPRINTF
-        #define FreeRTOS_printf( MSG )    if( ipconfigHAS_PRINTF ) configPRINTF( MSG )
+    #if ( ipconfigHAS_PRINTF == 1 ) && defined( configPRINTF )
+        #define FreeRTOS_printf( MSG )    do { configPRINTF( MSG ); } while( ipFALSE_BOOL )
     #else
         #define FreeRTOS_printf( MSG )    do {} while( ipFALSE_BOOL )
     #endif
diff --git a/test/cbmc/patches/FreeRTOSIPConfig.h b/test/cbmc/patches/FreeRTOSIPConfig.h
index 03d9164d62..f94bfb655a 100644
--- a/test/cbmc/patches/FreeRTOSIPConfig.h
+++ b/test/cbmc/patches/FreeRTOSIPConfig.h
@@ -37,12 +37,7 @@
 /* Set to 1 to print out debug messages.  If ipconfigHAS_DEBUG_PRINTF is set to
  * 1 then FreeRTOS_debug_printf should be defined to the function used to print
  * out the debugging messages. */
-#ifndef ipconfigHAS_DEBUG_PRINTF
-    #define ipconfigHAS_DEBUG_PRINTF    0
-#endif
-#if ( ipconfigHAS_DEBUG_PRINTF == 1 )
-    #define FreeRTOS_debug_printf( X )    configPRINTF( X )
-#endif
+#define FreeRTOS_debug_printf( X )
 
 /* Set to 1 to print out non debugging messages, for example the output of the
  * FreeRTOS_netstat() command, and ping replies.  If ipconfigHAS_PRINTF is set to 1