Loops with multiple phases are challenging to verify because they require disjunctive invariants. Invariants could also have the form of an implication between a precondition for the phase and a lemma that is valid throughout the phase. Such an invariant structure is not widely used in state-of-the-art verification approaches. This research presents a novel SMT-based approach to synthesize implication invariants for multi-phase loops. The technique computes Model Based Projections to discover the program’s phases, and leverages data learning to get relationships among loop variables at an arbitrary place in the loop. This approach has shown promising results in its ability to verify programs with complex phase structures.