How does one pick the proper loop invariant to prove an algorithm's correctness?

Question

We started with loop invariants last week and our professor proposed this question to work on at home. I've been following along the slides/lectures but I am having so much trouble with identifying a loop invariant which can help me prove the correctness of this algorithm.

Consider the following program which returns the least common multiple (LCM) of two natural numbers

// Pre : a, b are natural numbers
// Post : return LCM (a, b)
int GetLCM(int a, int b) {
    int x = a;
    int y = b;
    while (x != y) {
        if (x < y) {
            x = x + a;
        } else {
            y = y + b;
        }
    }
    return x;
}

I need to find the "proper loop invariant (Inv(x,y)) for this while-loop" which can aid me in proving its correctness. Are there multiple loop invariants which can be used to prove its correctness? I have a better understanding on proving an invariant using induction. However the initial process of picking a sufficient loop invariant(s) is confusing. If someone could lead me in the right direction or give me an example of the loop invariant in this while-loop, that would be much appreciated.

I understand that a loop invariant should be true before and immediately after every iteration of a loop. We did some word examples in class and it made a lot more sense, but when it comes to actually picking the loop invariant from some code I feel lost.