There are various kinds of static (and dynamic) verification frameworks and tools, all with weaknesses and strengths. Combining them manually or automatically is common by making different tools interoperate or by integrating various analyses in the same tool. In the SPARK verification tool for the Ada language, two static analyses work together: deductive verification and data+information flow analysis. Deductive verification offers strong guarantees at the cost of manual effort: users need to write contracts, and the guarantees are subject to a number of assumptions. Data+information flow analysis is used to alleviate some of these difficulties, thus making the tool easier to use. This article presents how the verification is shared between these analyses so that each one is used at its full potential and how they collaborate to improve the efficiency and precision of the SPARK tool while retaining soundness. If most of these collaborations are automated, a feature of SPARK lets the user choose which analysis should be used to verify initialization in a fine-grained manner, depending on their preferred trade-off.