Repair/RepairInterpreter/testmodel

   1 [forall u in UsedInode], u.inodestatus=literal(Used)
   2 [forall f in FreeInode], f.inodestatus=literal(Free)
   3 [forall u in UsedBlock], u.blockstatus=literal(Used)
   4 [forall f in FreeBlock], f.blockstatus=literal(Free)
   5 [forall i in UsedInode], i.referencecount=sizeof(i.~inodeof) or i in RootDirectoryInode
   6 [forall i in UsedInode], i.filesize <= sizeof(i.contents)*literal(8192)
   7 [forall b in FileDirectoryBlock],sizeof(b.~contents)=1
   8 [],sizeof(SuperBlock)=1
   9 [],sizeof(GroupBlock)=1
  10 [],sizeof(InodeTableBlock)=1
  11 [],sizeof(InodeBitmapBlock)=1
  12 [],sizeof(BlockBitmapBlock)=1
  13 [],sizeof(RootDirectoryInode)=1