SPECIFICATION Spec
INVARIANT AllAssertions

CONSTANT ModifiedCost <- DefectBodyCostClampVariant