2 type uref = { mutable cnt : int }
3 type dref = { mutable urf : uref }
4 type tref = { mutable drf : dref }
6 let che (t t1: tref) (d : dref)
7 ensures { t.drf.urf.cnt = 1 /\ t1.drf.urf.cnt = 0 }
8 = (t.drf, d.urf, t.drf.urf, t1.drf) <- (d, {cnt = 1}, {cnt = 0}, t.drf)
