Loop variant for a while loop that occasionally doesn't decrease?
Just a hint for now, since this is a practice problem: consider a lexicographic combination of orders.

In some more detail: Suppose you have two maps $f_1:S\to D_1$ and $f_2:S\to D_2$ from your program states $S$ into well-founded ordered domains $(D_1,\le_1)$ and  $(D_2,\le_2)$. The lexicographic combination of $\le_1$ and $\le_2$ is the order $\le$ on $D_1\times D_2$ given by $(x_1,y_1)\le(x_2,y_2)$ iff either $x_1\le_1x_2$, or $x_1=x_2,y_1\le_2y_2$. It is also well-founded.

So if $f_1,f_2$ are such that


$f_1$ never increases, and
whenever $f_1$ does not decrease, $f_2$ does,


then the map $(f_1,f_2):S\to D_1\times D_2$ is a variant proving termination.