Fixed a variety of bugs...

[repair.git] / Repair / RepairCompiler / MCC / specs / filesystem / test3.constraints

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 39d44626db78a758c41f02151d1b4a589ab21b0a..507a77fafd1fab6afcff16a43133ed23b7328e8d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
+++ b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
@@ -39,7 +39,7 @@
 // C7
 // ??? for all files and directory blocks check that
 // only one inode references this block
-[forall b in FileDirectoryBlock],sizeof(b.~contents)=1;
+[forall b in FileDirectoryBlock],sizeof(b.~contents)=1; // should be <=
 
 // C10
 // verify that there is one inodetableblock