verification - Dafny 事後条件メッセージに混乱

Question

非常に単純な乗算コード:

method Product1 (m: nat, n: nat) returns (res:nat) 
ensures res == m * n;      
{  
    var m1: nat := 0; 
    var n1: nat := 0; 
    res := 0; 
    while (m1 < m)    
   { 
    n1 := 0; 
    while (n1 < n)  
    { 
        res := res + 1;
        n1 := n1 + 1; 
    } 
    m1 := m1 + 1; 
    } 
}

ダフニーで確認すると、次のように表示されます。

     Description                                        Line Column
1   A postcondition might not hold on this return path. 8   4
2   This is the postcondition that might not hold.      2   16

いくつかの条件下で res != m*n と表示されますが、わかりません。