EXTRA-INFO

generate markers to indicate sources of guard proof obligations
Major Section:  GUARD

See guard-debug for a discussion of this function, which is useful for debugging failures during guard verification.