diff --git a/src/filo-fs-ext2.adb b/src/filo-fs-ext2.adb
index a69730e..d7bd018 100644
--- a/src/filo-fs-ext2.adb
+++ b/src/filo-fs-ext2.adb
@@ -715,10 +715,12 @@
          Cache_Start => Cache_Start,
          Cache_End   => Cache_End,
          Success     => Success);
+      Success := Success and then
+         -- TODO: Prove this using a predicate on Mount_State:
+         Cache_Start <= Cache_End - Group_In_Block_Offset - Static.Group_Desc_Size + 1;
       if not Success then
          return;
       end if;
-      pragma Assert_And_Cut (Cache_End = Cache_Start + Static.Block_Size - 1);
 
       Parse_Group
         (Static      => Static,
@@ -729,7 +731,6 @@
       if not Success then
          return;
       end if;
-      pragma Assert_And_Cut (Boolean'(True));
 
       declare
          Inode_In_Group : constant Inode_In_Group_Index :=
@@ -745,7 +746,6 @@
             Success := False;
             return;
          end if;
-         pragma Assert_And_Cut (First_Table_Block + Inode_Block in FSBlock_Offset);
 
          Cache_FSBlock
            (Static      => Static,
@@ -755,6 +755,9 @@
             Cache_Start => Cache_Start,
             Cache_End   => Cache_End,
             Success     => Success);
+         Success := Success and then
+            -- TODO: Prove this using a predicate on Mount_State:
+            Cache_Start <= Cache_End - Inode_In_Block_Offset - Static.Inode_Size + 1;
          if not Success then
             return;
          end if;