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