Indirect Record Update

[DavePearce]

For reasons unknown, the following fails to verify:

type state is ({int x, int y} this)
type pState is (&state this)

assert "assertion failed":
    forall(pState p1, pState p2):
        if:
            *p2 == *p1{x:=0}
        then:
            *p2.x == 0

The failing proof is:

73. exists(pState p1, pState p2).(((((*p2) == (*p1){x:=0})) && (((*p2).x != () 
 76. exists(pState p1, pState p2).(((*p2) == (*p1){x:=0}) && (0 != (* (Simp 73) 
 75. ((*p2) == (*p1){x:=0}) && (0 != (*p2).x)                     (Exists-E 76) 
 65. (*p2) == (*p1){x:=0}                                            (And-E 75) 
 74. 0 != (*p2).x                                                    (And-E 75) 
 83. ((*p2).x >= (0 + 1)) || (0 >= ((*p2).x + 1))                    (Neq-C 74) 
 87. ((*p2).x >= 1) || (0 >= (1 + (*p2).x))                           (Simp 83) 
┌──────────────────────────────────────────────────────────────────────────────┐
│ 84. (*p2).x >= 1                                                   (Or-E 87) │
├──────────────────────────────────────────────────────────────────────────────┤
│ 86. 0 >= (1 + (*p2).x)                                             (Or-E 87) │
└──────────────────────────────────────────────────────────────────────────────┘

In contrast, if we remove the references + dereferencing, then the proof is:

 67. exists(pState p1, pState p2).((((p2 == p1{x:=0})) && ((p2.x != 0))))    () 
 70. exists(pState p1, pState p2).((p2 == p1{x:=0}) && (0 != p2.x))   (Simp 67) 
 69. (p2 == p1{x:=0}) && (0 != p2.x)                              (Exists-E 70) 
 59. p2 == p1{x:=0}                                                  (And-E 69) 
 68. 0 != p2.x                                                       (And-E 69) 
 72. 0 != p1{x:=0}.x                                               (Eq-S 68,59) 
 52. false                                                            (Simp 72)

In the failing version, it doesn't seem to infer the equivalent of 72

[DavePearce]

UPDATE: the problem is that CongruenceClosure.rearrangeToAssignment(Formula) fails for (*p2) == (*p1){x:=0} but not for p2 == p1{x:=0}.

UPDATE: this is because rearrangeToAssignment(Formula) only rearranges equalities involving variables.