Failing Verification from WhileyCompiler

[DavePearce]

The following fails verification when compiled via WyC:

function reverse(int[] ls) -> int[]:
    int i = |ls|
    int[] r = [0; |ls|]
    while i > 0 where i <= |ls| && |r| == |ls|:
        int item = ls[|ls|-i]
        i = i - 1
        r[i] = item
    return r

However, the generated verification conditions are easily dispatched using wy verify. The failing proof is:

 482. exists(int i, int[] ls).((((i == |ls|)) && ((0 >= (|ls| + 1)))))       () 
 486. exists(int i, int[] ls).((i == |ls|) && (0 >= (1 + |ls|)))     (Simp 482) 
 485. (i == |ls|) && (0 >= (1 + |ls|))                           (Exists-E 486) 
 474. i == |ls|                                                     (And-E 485) 
 484. 0 >= (1 + |ls|)                                               (And-E 485) 
 488. 0 >= (1 + i)                                               (Eq-S 484,474) 
./While_Valid_1.whiley:5: negative length possible
    int[] r = [0; |ls|]
              ^^^^^^^^^

Whilst the passing version is:

 530. exists(int i, int[] ls).((((i == |ls|)) && ((0 >= (|ls| + 1)))))       () 
 534. exists(int i, int[] ls).((i == |ls|) && (0 >= (1 + |ls|)))     (Simp 530) 
 533. (i == |ls|) && (0 >= (1 + |ls|))                           (Exists-E 534) 
 532. 0 >= (1 + |ls|)                                               (And-E 533) 
 535. |ls| >= 0                                                  (ArrLen-I 532) 
 521. false                                                     (Ieq-I 535,532) 

[DavePearce]

With nonces enabled we have:

 482. exists(int i'20, int[] ls'15).((((i'20 == |ls'15|)) && ((0 >= (|ls'15| () 
 486. exists(int i'20, int[] ls'15).((i'20 == |ls'15|) && (0 >= (1 + (Simp 482) 
 485. (i'20 == |ls'15|) && (0 >= (1 + |ls'15|))                  (Exists-E 486) 
 474. i'20 == |ls'15|                                               (And-E 485) 
 484. 0 >= (1 + |ls'15|)                                            (And-E 485) 
 488. 0 >= (1 + i'20)                                            (Eq-S 484,474)

versus

 530. exists(int i'42, int[] ls'46).((((i'42 == |ls'46|)) && ((0 >= (|ls'46| () 
 534. exists(int i'42, int[] ls'46).((i'42 == |ls'46|) && (0 >= (1 + (Simp 530) 
 533. (i'42 == |ls'46|) && (0 >= (1 + |ls'46|))                  (Exists-E 534) 
 532. 0 >= (1 + |ls'46|)                                            (And-E 533) 
 535. |ls'46| >= 0                                               (ArrLen-I 532) 
 521. false                                                     (Ieq-I 535,532)

Yes, in the first we have i'20 versus ls'15 whilst in the second we have i'42 versus ls'46. This looks like a variable ordering problem.

[DavePearce]

Fixed following #136 and #138