multiple decreases lines (is this a bug?)

I played with Dafny and the exercises from Leino's book.
Exercise 3.5 asks for a decreases clause to prove the termination of the following function:

function K(x: nat, y: nat, z: nat): int
{
    if x < 10 || y < 5 
    then x + y
    else if z == 0
        then K(x-1, y, 5)
        else K(x, y-1, z-1)
}

Now, I added the clause "decreases x + y" which works fine (as expected).
But what also works is "decreases 6*(x+y) + z" (also as expected).
What does not work is "decreases 5*(x+y) + z" (also as expected).

But what surprised me is that I can have two (or even more) decreases clauses, and it appears that as soon as one of the decreases works, the others are happily accepted (or should I say ignored?).

Is that a bug, or intended behavior (in which case I miss the point)?

function K(x: nat, y: nat, z: nat): int
    decreases 5*(x+y) + z
    decreases x+y
{
    if x < 10 || y < 5 
    then x + y
    else if z == 0
        then K(x-1, y, 5)
        else K(x, y-1, z-1)
}

This is accepted by Dafny, but if you comment out the "decreases x+y" line, it fails (and that is correct).

Quoting from Dafny reference manual (https://dafny.org/dafny/DafnyRef/DafnyRef#sec-decreases-clause)

> Decreases clauses are used to prove termination in the presence of
> recursion. If more than one decreases clause is given it is as if a
> single decreases clause had been given with the collected list of
> arguments and a collected list of Attributes. That is,
>
> decreases A, B decreases C, D
>
> is equivalent to
>
> decreases A, B, C, D
>
> Note that changing the order of multiple decreases clauses will change
> the order of the expressions within the equivalent single decreases
> clause, and will therefore have different semantics.
>
> Termination metrics in Dafny, which are declared by decreases clauses,
> are lexicographic tuples of expressions. At each recursive (or
> mutually recursive) call to a function or method, Dafny checks that
> the effective decreases clause of the callee is strictly smaller than
> the effective decreases clause of the caller.

As long as decreases clauses tuple is lexicographically decreasing, it is good termination measure. In above case dafny is using 5*(x+y)+z, x+y as decrease clauses tuple.

In if branch of z==0, 5*(x+y)+z expression has same value in recursive call whereas x+y is decreasing. In then branch 5*(x+y)+z expression itself is decreasing. It is mere coincidence here that first decrease clause is either remains constant or decreases and when it remain constant another decrease clause after it indeed decreases.

To give counter example of one of clauses hypothesis consider following program

function K(x: nat, y: nat, z: nat): int
    decreases z
    decreases x + y
{
    if x < 10 || y < 5 
    then x + y
    else if z == 0
        then K(x-1, y, 5)
        else K(x, y-1, z-1)
}

Thanks Divyanshu Ranjan for answering my question.

Indeed, it turns out that you are right.

If I add another clause, being "decreases x-y" as the last clause, where it does not matter, it indeed works. If I make it the first clause, then it fails (as it should be). So, mystery solved (and it is not a bug).

Thanks!