Change to the spec...missed a consistency property. Adding timing option.
[repair.git] / Repair / RepairCompiler / MCC / specs / abiword / abi.constraints
index 5ea646d..ea14482 100755 (executable)
@@ -5,3 +5,4 @@
 [forall f in Frags], (sizeof(f.~Next)<=1);
 [forall f in firstblock], sizeof(f.~Next)=0;
 [forall l in Last, forall f in Fragments], f.PLast=l and sizeof(f.PLast)=1;
+[forall f in Frags], f.Length>=1;
\ No newline at end of file