diff --git a/certora/applyHarnessFifo.patch b/certora/applyHarnessFifo.patch
index 4f69001..4fad2fe 100644
--- a/certora/applyHarnessFifo.patch
+++ b/certora/applyHarnessFifo.patch
@@ -1,6 +1,6 @@
 diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
---- DoubleLinkedList.sol	2024-07-11 13:38:21.976522997 +0200
-+++ DoubleLinkedList.sol	2024-07-11 13:40:22.469518264 +0200
+--- DoubleLinkedList.sol	2024-07-12 09:49:49.899261374 +0200
++++ DoubleLinkedList.sol	2024-07-12 09:53:11.964303440 +0200
 @@ -16,6 +16,8 @@
  
      struct List {
@@ -10,15 +10,12 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
      }
  
      /* ERRORS */
-@@ -100,6 +102,7 @@
-         address next = list.accounts[address(0)].next; // `id` will be inserted before `next`.
- 
-         while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
+@@ -101,10 +103,12 @@
+         uint256 numberOfIterations;
+         for (; numberOfIterations < maxIterations; numberOfIterations++) {
+             if (next == address(0) || list.accounts[next].value < value) break;
 +            list.insertedAfter = next; // HARNESS
              next = list.accounts[next].next;
-             unchecked {
-                 ++numberOfIterations;
-@@ -107,6 +110,7 @@
          }
  
          if (numberOfIterations == maxIterations) next = address(0);
diff --git a/certora/applyHarnessSimple.patch b/certora/applyHarnessSimple.patch
index bcbedda..24b686d 100644
--- a/certora/applyHarnessSimple.patch
+++ b/certora/applyHarnessSimple.patch
@@ -1,6 +1,6 @@
 diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
---- DoubleLinkedList.sol	2024-07-11 13:38:21.976522997 +0200
-+++ DoubleLinkedList.sol	2024-07-11 13:40:08.765859975 +0200
+--- DoubleLinkedList.sol	2024-07-12 09:49:49.899261374 +0200
++++ DoubleLinkedList.sol	2024-07-12 09:52:16.333105454 +0200
 @@ -16,6 +16,8 @@
  
      struct List {
@@ -10,7 +10,7 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
      }
  
      /* ERRORS */
-@@ -90,23 +92,19 @@
+@@ -90,21 +92,20 @@
      /// @param list The list to search in.
      /// @param id The address of the account.
      /// @param value The value of the account.
@@ -21,16 +21,14 @@ diff -ruN DoubleLinkedList.sol DoubleLinkedList.sol
          if (id == address(0)) revert AddressIsZero();
          if (list.accounts[id].value != 0) revert AccountAlreadyInserted();
  
--        uint256 numberOfIterations;
          address next = list.accounts[address(0)].next; // `id` will be inserted before `next`.
  
--        while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
-+        while (next != address(0) && list.accounts[next].value >= value) {
+-        uint256 numberOfIterations;
+-        for (; numberOfIterations < maxIterations; numberOfIterations++) {
++        for (;;) {
+             if (next == address(0) || list.accounts[next].value < value) break;
 +            list.insertedAfter = next; // HARNESS
              next = list.accounts[next].next;
--            unchecked {
--                ++numberOfIterations;
--            }
          }
  
 -        if (numberOfIterations == maxIterations) next = address(0);
diff --git a/src/DoubleLinkedList.sol b/src/DoubleLinkedList.sol
index 867556b..fd305bf 100644
--- a/src/DoubleLinkedList.sol
+++ b/src/DoubleLinkedList.sol
@@ -96,14 +96,12 @@ library DoubleLinkedList {
         if (id == address(0)) revert AddressIsZero();
         if (list.accounts[id].value != 0) revert AccountAlreadyInserted();
 
-        uint256 numberOfIterations;
         address next = list.accounts[address(0)].next; // `id` will be inserted before `next`.
 
-        while (numberOfIterations < maxIterations && next != address(0) && list.accounts[next].value >= value) {
+        uint256 numberOfIterations;
+        for (; numberOfIterations < maxIterations; numberOfIterations++) {
+            if (next == address(0) || list.accounts[next].value < value) break;
             next = list.accounts[next].next;
-            unchecked {
-                ++numberOfIterations;
-            }
         }
 
         if (numberOfIterations == maxIterations) next = address(0);