Rearrangement in Congruence Closure

[DavePearce]

The following fails to verify:

assert "negative length possible":
    forall(int n, int[] a):
        if:
            |a| == n
        then:
            n >= 0

The generated proof is this:

 35. exists(int n, int[] a).((((|a| == n)) && ((0 >= (n + 1)))))             () 
 40. exists(int n, int[] a).((n == |a|) && (0 >= (1 + n)))            (Simp 35) 
 39. (n == |a|) && (0 >= (1 + n))                                 (Exists-E 40) 
 36. n == |a|                                                        (And-E 39) 
 38. 0 >= (1 + n)                                                    (And-E 39) 

In contrast, this minor variation does verify:

assert "negative length possible":
    forall(int n, int[] a):
        if:
            n == |a|
        then:
            n >= 0

And the generated proof is:

 35. exists(int n, int[] a).((((n == |a|)) && ((0 >= (n + 1)))))             () 
 39. exists(int n, int[] a).((n == |a|) && (0 >= (1 + n)))            (Simp 35) 
 38. (n == |a|) && (0 >= (1 + n))                                 (Exists-E 39) 
 25. n == |a|                                                        (And-E 38) 
 37. 0 >= (1 + n)                                                    (And-E 38) 
 41. 0 >= (1 + |a|)                                                (Eq-S 37,25) 
 42. |a| >= 0                                                     (ArrLen-I 41) 
 24. false                                                        (Ieq-I 42,41) 

It's pretty odd that, given apparently the same initial state, we end up with a different outcome. The key issue revolves around the method CongruenceClosure.rearrangeToAssignment. In the first case, this gives:

REARRANGED: |a| := n

In the second case, this gives:

REARRANGED: n := |a|

This definitely explains the difference.

[DavePearce]

UPDATE: the essential problem comes down to this function:

private static boolean lessThan(Expr lhs, Expr rhs) {
    return lhs.getIndex() < rhs.getIndex();
}

It chooses whichever variable access expression comes first. This doesn't seem optimal!!