diff --git a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c
index 37ac9569d..19dc02147 100644
--- a/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c
+++ b/test/cbmc/proofs/MQTT_DeserializeAck/MQTT_DeserializeAck_harness.c
@@ -35,7 +35,6 @@ void harness()
 
     pIncomingPacket = allocateMqttPacketInfo( NULL );
     __CPROVER_assume( isValidMqttPacketInfo( pIncomingPacket ) );
-    __CPROVER_assume( IMPLIES( pIncomingPacket != NULL, pIncomingPacket->remainingLength < REMAINING_LENGTH_MAX ) );
 
     /* These are allocated for coverage of a NULL input. */
     pPacketId = malloc( sizeof( uint16_t ) );
diff --git a/test/cbmc/sources/mqtt_cbmc_state.c b/test/cbmc/sources/mqtt_cbmc_state.c
index bb643fd1b..7f96076ca 100644
--- a/test/cbmc/sources/mqtt_cbmc_state.c
+++ b/test/cbmc/sources/mqtt_cbmc_state.c
@@ -69,6 +69,11 @@ bool isValidMqttPacketInfo( const MQTTPacketInfo_t * pPacketInfo )
 {
     bool isValid = true;
 
+    if( pPacketInfo != NULL )
+    {
+        isValid = isValid && pPacketInfo->remainingLength < REMAINING_LENGTH_MAX;
+    }
+
     return isValid;
 }