diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index deb2d21..3d6c0eb 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -481,11 +481,15 @@
          Cache_End   :    out Max_Block_Index;
          Success     :    out Boolean)
       with
-         Pre => Logical_Off <= Logical,
-         Post => (if Success then
-                     Next <= Dynamic_Max_Index and then
-                     Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
-                     Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
+         Pre =>
+            Logical_Off <= Logical and
+            Dynamic_Max_Index = State.Static.Block_Size / Extent_Header_Size - 1,
+         Post =>
+            State.Static = State.Static'Old and
+            (if Success then
+               Next <= Dynamic_Max_Index and then
+               Cache_End = Cache_Start + State.Static.Block_Size - 1 and then
+               Extent_Logical (Cache (Cache_Start .. Cache_End), Next) <= Logical)
       is
       begin
          Cache_FSBlock
@@ -518,6 +522,7 @@
             if not Success then
                Next := 1;
             else
+               pragma Assert (Cache_End - Cache_Start + 1 = State.Static.Block_Size);
                Next := Bin_Search (Cache (Cache_Start .. Cache_End), Hdr_Entries);
             end if;
          end;
@@ -554,7 +559,8 @@
          Logical_Off := Index_Logical (Inline_Extents, Idx);
          loop
             pragma Loop_Invariant
-              (Depth > 0 and then
+              (State.Static = State.Static'Loop_Entry and then
+               Depth > 0 and then
                Depth in Extent_Depth and then
                Logical_Off <= Logical);
             Depth := Depth - 1;
@@ -583,7 +589,8 @@
       Success :=
          Length > 0 and then
          Logical_Off <= FSBlock_Logical'Last - Length and then
-         Logical < Logical_Off + Length;
+         Logical < Logical_Off + Length and then
+         FSBlock_Offset (Logical - Logical_Off) <= FSBlock_Offset'Last - Physical;
       if Success then
          Physical := Physical + FSBlock_Offset (Logical - Logical_Off);
       end if;