Change to the spec...missed a consistency property. Adding timing option.

[repair.git] / Repair / RepairCompiler / MCC / specs / abiword / abi.model

diff --git a/Repair/RepairCompiler/MCC/specs/abiword/abi.model b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
index 6e6a54e9663a99f0eb89d43549ca1c454327f288..1736391ff49dce1bdbab2180630e5e19cf63828a 100755 (executable)
--- a/Repair/RepairCompiler/MCC/specs/abiword/abi.model
+++ b/Repair/RepairCompiler/MCC/specs/abiword/abi.model
@@ -6,5 +6,6 @@
 [forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
 [forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
 [forall f in Frags], (f.m_next=null) => f in Last;
+[forall f in Frags], true => <f,f.m_length> in Length;
 [forall f in Fragments], !(f.m_pLast=null) => <f,f.m_pLast> in PLast;
-[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;
\ No newline at end of file
+[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;