diff --git a/FreeRTOS/Source b/FreeRTOS/Source
index 50a232183..47338393f 160000
--- a/FreeRTOS/Source
+++ b/FreeRTOS/Source
@@ -1 +1 @@
-Subproject commit 50a23218381574f2ba314109691e1de4f8456684
+Subproject commit 47338393f1f79558f6144213409f09f81d7c4837
diff --git a/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch
deleted file mode 100644
index 6acf1c89a..000000000
--- a/FreeRTOS/Test/CBMC/patches/0008-Remove-overflow-assert-from-xQueueGenericCreate.patch
+++ /dev/null
@@ -1,20 +0,0 @@
-diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
-index edd08b26e..259c609f4 100644
---- a/FreeRTOS/Source/queue.c
-+++ b/FreeRTOS/Source/queue.c
-@@ -394,8 +394,13 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
-          * zero in the case the queue is used as a semaphore. */
-         xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */
- 
--        /* Check for multiplication overflow. */
--        configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
-+        /*
-+         * Multiplication overflow check is commented out in CBMC test as it involves an
-+         * expensive division operation and consumes longer compute time against a wide
-+         * range of input combination in CBMC proof.
-+         *
-+         * configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
-+         */
- 
-         /* Allocate the queue and storage area.  Justification for MISRA
-          * deviation as follows:  pvPortMalloc() always ensures returned memory
diff --git a/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch
new file mode 100644
index 000000000..566544706
--- /dev/null
+++ b/FreeRTOS/Test/CBMC/patches/0009-Remove-overflow-asserts-from-xQueueGenericCreate.patch
@@ -0,0 +1,13 @@
+diff --git a/FreeRTOS/Source/queue.c b/FreeRTOS/Source/queue.c
+index b01dfd11f..b219b599a 100644
+--- a/FreeRTOS/Source/queue.c
++++ b/FreeRTOS/Source/queue.c
+@@ -395,7 +395,7 @@ BaseType_t xQueueGenericReset( QueueHandle_t xQueue,
+         xQueueSizeInBytes = ( size_t ) ( uxQueueLength * uxItemSize ); /*lint !e961 MISRA exception as the casts are only redundant for some ports. */
+ 
+         /* Check for multiplication overflow. */
+-        configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) );
++        /* configASSERT( ( uxItemSize == 0 ) || ( uxQueueLength == ( xQueueSizeInBytes / uxItemSize ) ) ); */
+ 
+         /* Check for addition overflow. */
+         configASSERT( ( sizeof( Queue_t ) + xQueueSizeInBytes ) >  xQueueSizeInBytes );