Fix comment

FreeRTOS · Jun 20, 2023 · ea41b16 · ea41b16
1 parent 5ae065e
commit ea41b16
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/test/cbmc/proofs/ARP/xCheckLoopback/xCheckLoopback_harness.c b/test/cbmc/proofs/ARP/xCheckLoopback/xCheckLoopback_harness.c
@@ -43,8 +43,8 @@ void harness()
     NetworkBufferDescriptor_t * pxNetworkBuffer;
     BaseType_t bReleaseAfterSend;
 
-    __CPROVER_assume( xBufferLength < ipconfigNETWORK_MTU );
-    __CPROVER_assume( ( bReleaseAfterSend == pdTRUE ) || ( bReleaseAfterSend == pdFALSE ) );
+    __CPROVER_assume( ( xBufferLength >= 0 ) &&
+                      ( xBufferLength < ipconfigNETWORK_MTU ) );
 
     pxNetworkBuffer = ( NetworkBufferDescriptor_t * ) safeMalloc( sizeof( NetworkBufferDescriptor_t ) );