CONSTANTS
    Correct = Correct
    SplitCloneAliases = SplitCloneAliases
    MergeCloneObjects = MergeCloneObjects
    CrossBackingLink = CrossBackingLink
    LinkedRuntimeRename = LinkedRuntimeRename
    UnstableAliasClone = UnstableAliasClone
    Mode = Correct

SPECIFICATION Spec
CHECK_DEADLOCK FALSE

INVARIANTS
    TypeOK
    LinkSafety