X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2Fspecs%2Ffilesystem%2Ftest3.constraints;h=507a77fafd1fab6afcff16a43133ed23b7328e8d;hb=0367aa153420baf3ba9b4e36ad4dc3e21ba34285;hp=39d44626db78a758c41f02151d1b4a589ab21b0a;hpb=5fce119f486868de52406c3effb5bed234e29a0a;p=repair.git

diff --git a/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints b/Repair/RepairCompiler/MCC/specs/filesystem/test3.constraints
index 39d4462..507a77f 100755
--- 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